Namespaces | |
| namespace | Asp |
| namespace | Cli |
| namespace | Detail |
| namespace | mt |
| namespace | SatElite |
| namespace | Test |
| namespace | this_thread |
Classes | |
| struct | Activity |
| Type storing a constraint's activity. More... | |
| class | Antecedent |
| Stores a reference to the constraint that implied a literal. More... | |
| class | Assignment |
| Stores assignment related information. More... | |
| class | BasicSatConfig |
| class | BasicSolve |
| struct | BasicSolveEvent |
| struct | BasicSolveOptions |
| class | CBConsequences |
| Enumerator for computing the brave/cautious consequences of a logic program. More... | |
| struct | CCMinRecursive |
| class | ClaspBerkmin |
| A variant of the BerkMin decision heuristic from the BerkMin Sat-Solver. More... | |
| class | ClaspConfig |
| class | ClaspError |
| class | ClaspFacade |
| Provides a simplified interface to the services of the clasp library. More... | |
| class | ClaspVmtf |
| Variable Move To Front decision strategies inspired by Siege. More... | |
| class | ClaspVsids_t |
| A variable state independent decision heuristic favoring variables that were active in recent conflicts. More... | |
| class | Clause |
| Class for representing a clause in a solver. More... | |
| class | ClauseCreator |
| A helper-class for creating/adding clauses. More... | |
| class | ClauseHead |
| (Abstract) base class for clause types. More... | |
| class | ClauseInfo |
| struct | ClauseRep |
| Primitive representation of a clause. More... | |
| struct | ClauseWatch |
| struct | compose_1 |
| An unary operator function that returns Op1(Op2(x)) More... | |
| struct | compose_2_1 |
| An unary operator function that returns OP1(OP2(x), OP3(x)) More... | |
| struct | compose_2_2 |
| A binary operator function that returns OP1(OP2(x), OP3(y)) More... | |
| class | Configuration |
| Interface for configuring a SharedContext object and its associated solvers. More... | |
| class | Constraint |
| Base class for (boolean) constraints to be used in a Solver. More... | |
| struct | Constraint_t |
| Constraint types distinguished by a Solver. More... | |
| struct | ContextParams |
| Parameters for a SharedContext object. More... | |
| struct | CoreStats |
| A struct for holding core statistics used by a solver. More... | |
| class | DecisionHeuristic |
| Base class for decision heuristics to be used in a Solver. More... | |
| class | DefaultLparseParser |
| class | DefaultMinimize |
| Minimization via branch and bound. More... | |
| class | DefaultUnfoundedCheck |
| Clasp's default unfounded set checker. More... | |
| struct | DeleteObject |
| An unary operator function that calls delete p. More... | |
| struct | DestroyObject |
| An unary operator function that calls p->destroy() More... | |
| class | DimacsParser |
| class | Distributor |
| Base class for distributing learnt knowledge between solvers. More... | |
| class | DomainHeuristic |
| A VSIDS heuristic supporting additional domain knowledge. More... | |
| struct | DomScore |
| Score type for DomainHeuristic. More... | |
| class | EnumerationConstraint |
| A solver-local (i.e. thread-local) constraint to support enumeration. More... | |
| class | Enumerator |
| Interface for supporting enumeration of models. More... | |
| struct | EnumOptions |
| Options for configuring enumeration. More... | |
| struct | Event |
| Base class for library events. More... | |
| struct | Event_t |
| class | EventHandler |
| struct | ExpectedQuantity |
| struct | ExtendedStats |
| A struct for holding (optional) extra statistics. More... | |
| struct | GenericWatch |
| Represents a generic watch in a Solver. More... | |
| struct | HeuParams |
| struct | Heuristic_t |
| Simple factory for decision heuristics. More... | |
| struct | identity |
| An unary operator function that simply returns its argument. More... | |
| struct | ImpliedList |
| A type for storing ImpliedLiteral objects. More... | |
| struct | ImpliedLiteral |
| Stores information about a literal that is implied on an earlier level than the current decision level. More... | |
| struct | Input_t |
| struct | IsNull |
| struct | JumpStats |
| A struct for holding (optional) jump statistics. More... | |
| class | LearntConstraint |
| Base class for learnt constraints. More... | |
| class | Literal |
| A literal is a variable or its negation. More... | |
| struct | LogEvent |
| A log message. More... | |
| class | Lookahead |
| Lookahead extends propagation with failed-literal detection. More... | |
| class | LoopFormula |
| Constraint for Loop-Formulas. More... | |
| class | LparseParser |
| class | MessageHandler |
| class | MinimizeBuilder |
| Helper class for creating minimize constraints. More... | |
| class | MinimizeConstraint |
| Base class for implementing (mulit-level) minimize statements. More... | |
| struct | MinimizeMode_t |
| Supported minimization modes. More... | |
| struct | Model |
| Type for storing a model. More... | |
| class | ModelEnumerator |
| Class for model enumeration with minimization and projection. More... | |
| struct | ModelEvent |
| Event type for reporting models via generic event handler. More... | |
| class | OPBParser |
| struct | PairContains |
| A predicate that checks whether a std::pair contains a certain value. More... | |
| struct | ParseError |
| Instances of this class are thrown if a problem occurs during parsing input. More... | |
| class | PBBuilder |
| A class for defining a PB-problem. More... | |
| class | PlatformError |
| struct | PodQueue |
| struct | PodVector |
| class | PostPropagator |
| Base class for post propagators. More... | |
| struct | Problem_t |
| struct | ProblemStats |
| struct | ProcessTime |
| class | ProgramBuilder |
| Interface for defining an input program. More... | |
| struct | QueueImpl |
| struct | Range |
| struct | RealTime |
| struct | ReasonStore32 |
| struct | ReasonStore64 |
| Type for storing reasons for variable assignments together with additional data. More... | |
| struct | ReduceParams |
| Aggregates parameters for the nogood deletion heuristic used during search. More... | |
| struct | ReduceStrategy |
| Reduce strategy used during solving. More... | |
| struct | ReleaseObject |
| An unary operator function that calls p->release() More... | |
| struct | RestartParams |
| Aggregates restart-parameters to configure restarts during search. More... | |
| class | Restricted |
| class | RNG |
| A very simple but fast Pseudo-random number generator. More... | |
| class | SatBuilder |
| A class for defining a SAT-problem in CNF. More... | |
| struct | SatPreParams |
| Parameters for (optional) Sat-preprocessing. More... | |
| class | SatPreprocessor |
| Base class for preprocessors working on clauses only. More... | |
| struct | ScheduleStrategy |
| Implements clasp's configurable schedule-strategies. More... | |
| struct | ScoreLook |
| A small helper class used to score the result of a lookahead operation. More... | |
| struct | SearchLimits |
| Parameter-Object for managing search limits. More... | |
| struct | select1st |
| An unary operator function that returns the first value of a std::pair. More... | |
| struct | select2nd |
| An unary operator function that returns the second value of a std::pair. More... | |
| class | SelectFirst |
| Selects the first free literal w.r.t to the initial variable order. More... | |
| class | SequentialSolve |
| class | SharedContext |
| Aggregates information to be shared between solver objects. More... | |
| class | SharedDependencyGraph |
| (Positive) Body-Atom-Dependency Graph. More... | |
| class | SharedLiterals |
| An array of literals that can be shared between threads. More... | |
| class | SharedMinimizeData |
| A type holding data (possibly) shared between a set of minimize constraints. More... | |
| class | ShortImplicationsGraph |
| A class for efficiently storing and propagating binary and ternary clauses. More... | |
| class | SingleOwnerPtr |
| class | SmallClauseAlloc |
| Allocator for small (at most 32-byte) clauses. More... | |
| class | SolveAlgorithm |
| Interface for complex solve algorithms. More... | |
| struct | SolveEvent |
| Base class for solving related events. More... | |
| struct | SolveLimits |
| Type for holding global solve limits. More... | |
| struct | SolveParams |
| Parameter-Object for grouping solve-related options. More... | |
| class | Solver |
| clasp's Solver class. More... | |
| struct | SolverParams |
| Parameter-Object for configuring a solver. More... | |
| struct | SolverStats |
| A struct for aggregating statistics maintained in a solver object. More... | |
| struct | SolverStrategies |
| struct | SolveTestEvent |
| class | StreamParser |
| class | StreamSource |
| struct | SumQueue |
| class | SymbolTable |
| Symbol table that maps external ids to internal literals. More... | |
| struct | ThreadTime |
| class | Timer |
| class | UncoreMinimize |
| Minimization via unsat cores. More... | |
| class | UnitHeuristic |
| Heuristic that uses the results of lookahead. More... | |
| class | UserConfiguration |
| Base class for user-provided configurations. More... | |
| struct | ValueSet |
| A set of configurable values for a variable. More... | |
| struct | Var_t |
| Possible types of a variable. More... | |
| struct | VarInfo |
| Stores static information about a variable. More... | |
| struct | VarScore |
| Type used to store lookahead-information for one variable. More... | |
| struct | VsidsScore |
| Score type for VSIDS heuristic. More... | |
| class | WeightConstraint |
| Class implementing smodels-like cardinality- and weight constraints. More... | |
| struct | WeightLitsRep |
| Primitive representation of weight constraint literals in normal form. More... | |
Typedefs | |
| typedef ClaspVsids_t< VsidsScore > | ClaspVsids |
| typedef Constraint_t::Type | ConstraintType |
| typedef Problem_t::Format | InputFormat |
| typedef PodVector< Literal >::type | LitVec |
| typedef MinimizeMode_t::Mode | MinimizeMode |
| typedef Problem_t::Type | ProblemType |
| typedef Range< uint32 > | Range32 |
| typedef Clasp::BasicSolveOptions | SolveOptions |
| typedef PodVector< wsum_t >::type | SumVec |
| typedef no_multi_threading::thread | thread |
| typedef Constraint_t::Set | TypeSet |
| typedef uint8 | ValueRep |
| typedef PodVector< ValueRep >::type | ValueVec |
| typedef uint32 | Var |
| A variable is currently nothing more but an integer in the range [0..varMax). | |
| typedef Var_t::Type | VarType |
| typedef PodVector< Var >::type | VarVec |
| typedef bk_lib::left_right_sequence < ClauseWatch, GenericWatch, 0 > | WatchList |
| Watch list type. | |
| typedef int32 | weight_t |
| A signed integer type used to represent weights. | |
| typedef std::pair< Literal, weight_t > | WeightLiteral |
| typedef PodVector < WeightLiteral >::type | WeightLitVec |
| typedef PodVector< weight_t >::type | WeightVec |
| typedef int64 | wsum_t |
| A signed integer type used to represent sums of weights. | |
Functions | |
| double | addR (uint32 idx, double a) |
| uint64 | choose (unsigned n, unsigned k) |
| ClauseHead * | clause (const Antecedent &ante) |
| template<class OP1 , class OP2 > | |
| compose_1< OP1, OP2 > | compose1 (const OP1 &op1, const OP2 &op2) |
| template<class OP1 , class OP2 , class OP3 > | |
| compose_2_1< OP1, OP2, OP3 > | compose2 (const OP1 &op1, const OP2 &op2, const OP3 &op3) |
| template<class OP1 , class OP2 , class OP3 > | |
| compose_2_2< OP1, OP2, OP3 > | compose22 (const OP1 &op1, const OP2 &op2, const OP3 &op3) |
| template<class ToType , class EvType > | |
| const ToType * | event_cast (const EvType &ev) |
| ValueRep | falseValue (const Literal &lit) |
| Returns the value that makes the literal lit false. | |
| double | growR (uint32 idx, double g) |
| template<class T > | |
| void | growVecTo (T &vec, typename T::size_type j, const typename T::value_type &val=typename T::value_type()) |
| unsigned | hashId (unsigned key) |
| uint32 | index (Var v) |
| Returns the index of variable v. | |
| bool | isRevLit (const Solver &s, Literal p, uint32 maxL) |
| bool | isSentinel (Literal p) |
| Returns true if p represents the special variable 0. | |
| bool | isStdIn (const std::string &in) |
| bool | isStdOut (const std::string &out) |
| uint32 | log2 (uint32 x) |
| uint32 | lubyR (uint32 idx) |
| bool | match (StreamSource &in, char c, bool sw) |
| Consumes next character if equal to c. | |
| bool | match (StreamSource &in, const char *str, bool sw) |
| Consumes string str. | |
| bool | matchEol (StreamSource &in, bool sw) |
| bool | matchStatPath (const char *&x, const char *path, std::size_t len) |
| bool | matchStatPath (const char *&x, const char *path) |
| LogEvent | message (Event::Subsystem sys, const char *what, const Solver *s=0) |
| Creates a low priority message event. | |
| uint32 | momsScore (const Solver &s, Var v) |
| Computes a moms-like score for var v. | |
| template<class T > | |
| void | moveDown (T &t, typename T::size_type from, typename T::size_type to) |
| Literal | negLit (Var v) |
| Creates the negative literal of variable v. | |
| bool | operator!= (const Literal &lhs, const Literal &rhs) |
| Returns !(lhs == rhs). | |
| bool | operator< (const Literal &lhs, const Literal &rhs) |
| Defines a strict-weak-ordering for Literals. | |
| std::ostream & | operator<< (std::ostream &os, Literal l) |
| std::istream & | operator>> (std::istream &in, Literal &l) |
| Literal | operator^ (Literal lhs, bool sign) |
| Literal | operator^ (bool sign, Literal rhs) |
| double | percent (uint64 x, uint64 y) |
| Literal | posLit (Var v) |
| Creates the positive literal of variable v. | |
| double | ratio (uint64 x, uint64 y) |
| bool | readLine (StreamSource &in, PodVector< char >::type &buf) |
| Extracts characters from in and stores them into buf until a newline character or eof is found. | |
| template<class T > | |
| void | releaseVec (T &t) |
| void | releaseVec (WatchList &w) |
| template<class C , class P > | |
| void | remove_first_if (C &cont, const P &p) |
| Removes from the container c the first occurrence of a value v for which p(v) returns true. | |
| template<class T > | |
| void | shrinkVecTo (T &t, typename T::size_type j) |
| template<class C > | |
| void | simplifyDB (Solver &s, C &db, bool shuffle) |
| void | skipLine (StreamSource &in) |
| Skips the current line. | |
| void | swap (Literal &l, Literal &r) |
| ValueRep | trueValue (const Literal &lit) |
| Returns the value that makes the literal lit true. | |
| bool | valSign (ValueRep v) |
| Returns the sign that matches the value. | |
| LogEvent | warning (Event::Subsystem sys, const char *what, const Solver *s=0) |
| Creates a high priority warning event. | |
| static int | xconvert (const char *x, ScheduleStrategy &out, const char **errPos, int e) |
Variables | |
| static BasicSatConfig | config_def_s |
| const uint32 | idMax = UINT32_MAX |
| Ids are integers in the range [0..idMax). | |
| static PostPropagator * | sent_list |
| const Var | sentVar = 0 |
| The variable 0 has a special meaning in the solver. | |
| const ValueRep | value_false = 2 |
| const ValueRep | value_free = 0 |
| const ValueRep | value_true = 1 |
| const Var | varMax = (Var(1) << 30) |
| varMax is not a valid variale, i.e. currently Clasp supports at most 2^30 variables. | |
| typedef ClaspVsids_t<VsidsScore> Clasp::ClaspVsids |
Definition at line 306 of file heuristics.h.
| typedef Problem_t::Format Clasp::InputFormat |
Definition at line 35 of file claspfwd.h.
Definition at line 52 of file minimize_constraint.h.
| typedef Problem_t::Type Clasp::ProblemType |
Definition at line 34 of file claspfwd.h.
| typedef Range<uint32> Clasp::Range32 |
Definition at line 191 of file solver_strategies.h.
Definition at line 49 of file clasp_facade.h.
| double Clasp::addR | ( | uint32 | idx, |
| double | a | ||
| ) |
Definition at line 77 of file solver_strategies.cpp.
| ClauseHead* Clasp::clause | ( | const Antecedent & | ante | ) | [inline] |
Definition at line 917 of file solver.cpp.
| const ToType* Clasp::event_cast | ( | const EvType & | ev | ) |
Definition at line 81 of file misc_types.h.
| double Clasp::growR | ( | uint32 | idx, |
| double | g | ||
| ) |
Definition at line 76 of file solver_strategies.cpp.
| void Clasp::growVecTo | ( | T & | vec, |
| typename T::size_type | j, | ||
| const typename T::value_type & | val = typename T::value_type() |
||
| ) | [inline] |
Definition at line 58 of file pod_vector.h.
| bool Clasp::isStdIn | ( | const std::string & | in | ) | [inline] |
Definition at line 49 of file clasp_app.cpp.
| bool Clasp::isStdOut | ( | const std::string & | out | ) | [inline] |
Definition at line 50 of file clasp_app.cpp.
| uint32 Clasp::log2 | ( | uint32 | x | ) | [inline] |
Definition at line 85 of file solver_strategies.h.
| uint32 Clasp::lubyR | ( | uint32 | idx | ) |
Definition at line 78 of file solver_strategies.cpp.
| bool Clasp::match | ( | StreamSource & | in, |
| char | c, | ||
| bool | sw | ||
| ) | [inline] |
Consumes next character if equal to c.
| in | StreamSource from which characters should be read |
| c | character to match |
| sw | skip leading spaces |
| bool Clasp::match | ( | StreamSource & | in, |
| const char * | str, | ||
| bool | sw | ||
| ) | [inline] |
Consumes string str.
| in | StreamSource from which characters should be read |
| str | string to match |
| sw | skip leading spaces |
| bool Clasp::matchEol | ( | StreamSource & | in, |
| bool | sw | ||
| ) | [inline] |
| LogEvent Clasp::message | ( | Event::Subsystem | sys, |
| const char * | what, | ||
| const Solver * | s = 0 |
||
| ) | [inline] |
Creates a low priority message event.
Definition at line 64 of file misc_types.h.
| uint32 Clasp::momsScore | ( | const Solver & | s, |
| Var | v | ||
| ) |
Computes a moms-like score for var v.
Definition at line 33 of file heuristics.cpp.
| void Clasp::moveDown | ( | T & | t, |
| typename T::size_type | from, | ||
| typename T::size_type | to | ||
| ) |
Definition at line 66 of file pod_vector.h.
| std::ostream & Clasp::operator<< | ( | std::ostream & | os, |
| Literal | l | ||
| ) | [inline] |
Definition at line 37 of file clasp_app.cpp.
| std::istream& Clasp::operator>> | ( | std::istream & | in, |
| Literal & | l | ||
| ) | [inline] |
Definition at line 42 of file clasp_app.cpp.
| bool Clasp::readLine | ( | StreamSource & | in, |
| PodVector< char >::type & | buf | ||
| ) |
Extracts characters from in and stores them into buf until a newline character or eof is found.
Definition at line 110 of file parser.cpp.
| void Clasp::releaseVec | ( | T & | t | ) | [inline] |
Definition at line 48 of file pod_vector.h.
| void Clasp::shrinkVecTo | ( | T & | t, |
| typename T::size_type | j | ||
| ) | [inline] |
Definition at line 53 of file pod_vector.h.
| void Clasp::skipLine | ( | StreamSource & | in | ) | [inline] |
| LogEvent Clasp::warning | ( | Event::Subsystem | sys, |
| const char * | what, | ||
| const Solver * | s = 0 |
||
| ) | [inline] |
Creates a high priority warning event.
Definition at line 68 of file misc_types.h.
| static int Clasp::xconvert | ( | const char * | x, |
| ScheduleStrategy & | out, | ||
| const char ** | errPos, | ||
| int | e | ||
| ) | [static] |
Definition at line 80 of file clasp_options.cpp.
BasicSatConfig Clasp::config_def_s [static] |
Definition at line 480 of file shared_context.cpp.
PostPropagator* Clasp::sent_list [static] |
Definition at line 45 of file solver.cpp.