|
clingo
|
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Groups
|
clingo
|
Aggregates information to be shared between solver objects. More...
#include <shared_context.h>
Public Types | |
| enum | InitMode { init_share_symbols, init_copy_symbols } |
| typedef SharedDependencyGraph | SDG |
| typedef PodVector< Solver * >::type | SolverVec |
| typedef SingleOwnerPtr< SDG > | SccGraph |
| typedef Configuration * | ConfigPtr |
| typedef SingleOwnerPtr < Distributor > | DistrPtr |
| typedef const ProblemStats & | StatsRef |
| typedef SymbolTable & | SymbolsRef |
| typedef LitVec::size_type | size_type |
| typedef ShortImplicationsGraph | ImpGraph |
| typedef const ImpGraph & | ImpGraphRef |
| typedef EventHandler * | LogPtr |
| typedef SingleOwnerPtr < SatPreprocessor > | SatPrePtr |
Public Member Functions | |
Problem introspection | |
Functions for querying information about the problem. | |
| bool | ok () const |
| Returns true unless the master has an unresolvable top-level conflict. More... | |
| bool | frozen () const |
| Returns whether the problem is currently frozen and therefore ready for being solved. More... | |
| bool | isShared () const |
| Returns whether more than one solver is actively working on the problem. More... | |
| bool | isExtended () const |
| bool | hasSolver (uint32 id) const |
| Returns whether this object has a solver associcated with the given id. More... | |
| Solver * | master () const |
| Returns the master solver associated with this object. More... | |
| Solver * | solver (uint32 id) const |
| Returns the solver with the given id. More... | |
| uint32 | numVars () const |
| Returns the number of problem variables. More... | |
| uint32 | numEliminatedVars () const |
| Returns the number of eliminated vars. More... | |
| bool | validVar (Var var) const |
| Returns true if var represents a valid variable in this problem. More... | |
| VarInfo | varInfo (Var v) const |
| Returns information about the given variable. More... | |
| bool | eliminated (Var v) const |
| Returns true if v is currently eliminated, i.e. no longer part of the problem. More... | |
| bool | marked (Literal p) const |
| Literal | stepLiteral () const |
| uint32 | numConstraints () const |
| Returns the number of problem constraints. More... | |
| uint32 | numBinary () const |
| Returns the number of binary constraints. More... | |
| uint32 | numTernary () const |
| Returns the number of ternary constraints. More... | |
| uint32 | numUnary () const |
| Returns the number of unary constraints. More... | |
| uint32 | problemComplexity () const |
| Returns an estimate of the problem complexity based on the number and type of constraints. More... | |
| StatsRef | stats () const |
| SymbolsRef | symbolTable () const |
Problem setup | |
Functions for specifying the problem. Problem specification is a four-stage process:
| |
| bool | unfreeze () |
| Unfreezes a frozen program and prepares it for updates. More... | |
| void | cloneVars (const SharedContext &other, InitMode m=init_copy_symbols) |
| Clones vars and symbol table from other. More... | |
| void | resizeVars (uint32 maxVar) |
| Sets the range of problem variables to [1, maxVar) More... | |
| Var | addVar (VarType t, bool eq=false) |
| Adds a new variable of type t. More... | |
| void | requestStepVar () |
| Requests a special variable for tagging volatile knowledge in incremental setting. More... | |
| void | requestData (Var v) |
| Request additional reason data slot for variable v. More... | |
| void | setFrozen (Var v, bool b) |
| Freezes/defreezes a variable (a frozen var is exempt from Sat-preprocessing). More... | |
| void | setNant (Var v, bool b) |
| Marks/unmarks v as contained in a negative loop or head of a choice rule. More... | |
| void | setInDisj (Var v, bool b) |
| Marks/unmarks v as contained in a non-hcf disjunction. More... | |
| void | setProject (Var v, bool b) |
| Marks/unmarks v as projection variable. More... | |
| void | setVarEq (Var v, bool b) |
| void | mark (Literal p) |
| void | unmark (Var v) |
| void | eliminate (Var v) |
| Eliminates the variable v from the problem. More... | |
| Solver & | startAddConstraints (uint32 constraintGuess=100) |
| Prepares the master solver so that constraints can be added. More... | |
| bool | addUnary (Literal x) |
| A convenience method for adding facts to the master. More... | |
| bool | addBinary (Literal x, Literal y) |
| A convenience method for adding binary clauses. More... | |
| bool | addTernary (Literal x, Literal y, Literal z) |
| A convenience method for adding ternary clauses. More... | |
| void | add (Constraint *c) |
| A convenience method for adding constraints to the master. More... | |
| bool | endInit (bool attachAll=false) |
| Finishes initialization of the master solver. More... | |
Configuration | |
| SatPrePtr | satPrepro |
| SccGraph | sccGraph |
| SharedContext () | |
| Creates a new object for sharing variables and the binary and ternary implication graph. More... | |
| ~SharedContext () | |
| void | reset () |
| Resets this object to the state after default construction. More... | |
| void | setEventHandler (EventHandler *r) |
| Enables event reporting via the given event handler. More... | |
| void | setShareMode (ContextParams::ShareMode m) |
| Sets how to handle physical sharing of constraints. More... | |
| void | setShortMode (ContextParams::ShortMode m) |
| Sets whether the short implication graph should be used for storing short learnt constraints. More... | |
| void | setConcurrency (uint32 numSolver) |
| Sets maximal number of solvers sharing this object. More... | |
| Solver & | addSolver () |
| Adds an additional solver to this object and returns it. More... | |
| void | enableStats (uint32 level) |
| Configures the statistic object of attached solvers. More... | |
| void | accuStats () |
| void | setPreserveModels (bool b=true) |
| If b is true, sets preprocessing mode to model-preserving operations only. More... | |
| void | setConfiguration (Configuration *c, bool own) |
| Sets the configuration for this object and its attached solvers. More... | |
| ConfigPtr | configuration () const |
| Returns the current configuration used in this object. More... | |
| LogPtr | eventHandler () const |
| Returns the active event handler or 0 if none was set. More... | |
| bool | seedSolvers () const |
| Returns whether this object seeds the RNG of new solvers. More... | |
| uint32 | concurrency () const |
| Returns the number of solvers that can share this object. More... | |
| bool | preserveModels () const |
| bool | physicalShare (ConstraintType t) const |
| Returns whether physical sharing is enabled for constraints of type t. More... | |
| bool | physicalShareProblem () const |
| Returns whether pyhiscal sharing of problem constraints is enabled. More... | |
| bool | allowImplicit (ConstraintType t) const |
| Returns whether short constraints of type t can be stored in the short implication graph. More... | |
(Parallel) solving | |
Functions to be called during (parallel) solving.
| |
| DistrPtr | distributor |
| bool | attach (uint32 id) |
| Attaches the solver with the given id to this object. More... | |
| bool | attach (Solver &s) |
| void | detach (uint32 id, bool reset=false) |
| Detaches the solver with the given id from this object. More... | |
| void | detach (Solver &s, bool reset=false) |
| uint32 | winner () const |
| void | setWinner (uint32 sId) |
| void | simplify (bool shuffle) |
| Simplifies the problem constraints w.r.t the master's assignment. More... | |
| void | removeConstraint (uint32 idx, bool detach) |
| Removes the constraint with the given idx from the master's db. More... | |
| int | addImp (ImpGraph::ImpType t, const Literal *lits, ConstraintType ct) |
| Adds the given short implication to the short implication graph if possible. More... | |
| uint32 | numLearntShort () const |
| Returns the number of learnt short implications. More... | |
| ImpGraphRef | shortImplications () const |
| void | simplifyShort (const Solver &s, Literal p) |
| void | report (const Event &ev) const |
| bool | report (const Solver &s, const Model &m) const |
| void | initStats (Solver &s) const |
| const SolverStats & | stats (const Solver &s, bool accu) const |
Aggregates information to be shared between solver objects.
Among other things, SharedContext objects store static information on variables, the (possibly unused) symbol table, as well as the binary and ternary implication graph of the input problem.
Furthermore, a SharedContext object always stores a distinguished master solver that is used to store and simplify problem constraints. Additional solvers can be added via SharedContext::addSolver(). Once initialization is completed, any additional solvers must be attached to this object by calling SharedContext::attach().
| typedef const ImpGraph& Clasp::SharedContext::ImpGraphRef |
| typedef EventHandler* Clasp::SharedContext::LogPtr |
| typedef LitVec::size_type Clasp::SharedContext::size_type |
| typedef PodVector<Solver*>::type Clasp::SharedContext::SolverVec |
| typedef const ProblemStats& Clasp::SharedContext::StatsRef |
|
explicit |
Creates a new object for sharing variables and the binary and ternary implication graph.
| Clasp::SharedContext::~SharedContext | ( | ) |
| void Clasp::SharedContext::accuStats | ( | ) |
| void Clasp::SharedContext::add | ( | Constraint * | c | ) |
A convenience method for adding constraints to the master.
A convenience method for adding binary clauses.
| int Clasp::SharedContext::addImp | ( | ImpGraph::ImpType | t, |
| const Literal * | lits, | ||
| ConstraintType | ct | ||
| ) |
Adds the given short implication to the short implication graph if possible.
| Solver & Clasp::SharedContext::addSolver | ( | ) |
Adds an additional solver to this object and returns it.
A convenience method for adding ternary clauses.
| bool Clasp::SharedContext::addUnary | ( | Literal | x | ) |
A convenience method for adding facts to the master.
Adds a new variable of type t.
| t | Type of the new variable (either Var_t::atom_var or Var_t::body_var). |
| eq | True if var represents both an atom and a body. In that case t is the variable's primary type and determines the preferred literal. |
|
inline |
Returns whether short constraints of type t can be stored in the short implication graph.
|
inline |
Attaches the solver with the given id to this object.
| bool Clasp::SharedContext::attach | ( | Solver & | s | ) |
| void Clasp::SharedContext::cloneVars | ( | const SharedContext & | other, |
| InitMode | m = init_copy_symbols |
||
| ) |
Clones vars and symbol table from other.
|
inline |
Returns the number of solvers that can share this object.
|
inline |
Returns the current configuration used in this object.
|
inline |
Detaches the solver with the given id from this object.
The function removes any tentative constraints from s. Shall be called once after search has stopped.
| void Clasp::SharedContext::detach | ( | Solver & | s, |
| bool | reset = false |
||
| ) |
| void Clasp::SharedContext::eliminate | ( | Var | v | ) |
Eliminates the variable v from the problem.
| bool Clasp::SharedContext::eliminated | ( | Var | v | ) | const |
Returns true if v is currently eliminated, i.e. no longer part of the problem.
| void Clasp::SharedContext::enableStats | ( | uint32 | level | ) |
Configures the statistic object of attached solvers.
The level determines the amount of extra statistics. Currently two levels are supported:
| bool Clasp::SharedContext::endInit | ( | bool | attachAll = false | ) |
Finishes initialization of the master solver.
The function must be called once before search is started. After endInit() was called, previously added solvers can be attached to the shared context and learnt constraints may be added to solver.
| attachAll | If true, also calls attach() for all solvers that were added to this object. |
|
inline |
Returns the active event handler or 0 if none was set.
|
inline |
Returns whether the problem is currently frozen and therefore ready for being solved.
|
inline |
Returns whether this object has a solver associcated with the given id.
| void Clasp::SharedContext::initStats | ( | Solver & | s | ) | const |
|
inline |
|
inline |
Returns whether more than one solver is actively working on the problem.
|
inline |
|
inline |
|
inline |
Returns the master solver associated with this object.
|
inline |
Returns the number of binary constraints.
| uint32 Clasp::SharedContext::numConstraints | ( | ) | const |
Returns the number of problem constraints.
|
inline |
Returns the number of eliminated vars.
|
inline |
Returns the number of learnt short implications.
|
inline |
Returns the number of ternary constraints.
|
inline |
Returns the number of unary constraints.
|
inline |
| bool Clasp::SharedContext::ok | ( | ) | const |
Returns true unless the master has an unresolvable top-level conflict.
|
inline |
Returns whether physical sharing is enabled for constraints of type t.
|
inline |
Returns whether pyhiscal sharing of problem constraints is enabled.
|
inline |
| uint32 Clasp::SharedContext::problemComplexity | ( | ) | const |
Returns an estimate of the problem complexity based on the number and type of constraints.
| void Clasp::SharedContext::removeConstraint | ( | uint32 | idx, |
| bool | detach | ||
| ) |
Removes the constraint with the given idx from the master's db.
|
inline |
| void Clasp::SharedContext::requestData | ( | Var | v | ) |
Request additional reason data slot for variable v.
| void Clasp::SharedContext::requestStepVar | ( | ) |
Requests a special variable for tagging volatile knowledge in incremental setting.
| void Clasp::SharedContext::reset | ( | ) |
Resets this object to the state after default construction.
|
inline |
Sets the range of problem variables to [1, maxVar)
|
inline |
Returns whether this object seeds the RNG of new solvers.
| void Clasp::SharedContext::setConcurrency | ( | uint32 | numSolver | ) |
Sets maximal number of solvers sharing this object.
| void Clasp::SharedContext::setConfiguration | ( | Configuration * | c, |
| bool | own | ||
| ) |
Sets the configuration for this object and its attached solvers.
|
inline |
Enables event reporting via the given event handler.
| void Clasp::SharedContext::setFrozen | ( | Var | v, |
| bool | b | ||
| ) |
Freezes/defreezes a variable (a frozen var is exempt from Sat-preprocessing).
|
inline |
Marks/unmarks v as contained in a non-hcf disjunction.
|
inline |
Marks/unmarks v as contained in a negative loop or head of a choice rule.
|
inline |
If b is true, sets preprocessing mode to model-preserving operations only.
|
inline |
Marks/unmarks v as projection variable.
| void Clasp::SharedContext::setShareMode | ( | ContextParams::ShareMode | m | ) |
Sets how to handle physical sharing of constraints.
| void Clasp::SharedContext::setShortMode | ( | ContextParams::ShortMode | m | ) |
Sets whether the short implication graph should be used for storing short learnt constraints.
|
inline |
|
inline |
|
inline |
| void Clasp::SharedContext::simplify | ( | bool | shuffle | ) |
Simplifies the problem constraints w.r.t the master's assignment.
|
inline |
Returns the solver with the given id.
| Solver & Clasp::SharedContext::startAddConstraints | ( | uint32 | constraintGuess = 100 | ) |
Prepares the master solver so that constraints can be added.
Must be called to publish previously added variables to master solver and before constraints over these variables can be added.
|
inline |
| const SolverStats & Clasp::SharedContext::stats | ( | const Solver & | s, |
| bool | accu | ||
| ) | const |
|
inline |
|
inline |
| bool Clasp::SharedContext::unfreeze | ( | ) |
Unfreezes a frozen program and prepares it for updates.
The function also triggers forgetting of volatile knowledge and removes any auxiliary variables.
|
inline |
|
inline |
Returns true if var represents a valid variable in this problem.
Returns information about the given variable.
|
inline |
| DistrPtr Clasp::SharedContext::distributor |
Distributor object to use for distribution of learnt constraints.
| SatPrePtr Clasp::SharedContext::satPrepro |
Preprocessor for simplifying problem.
| SccGraph Clasp::SharedContext::sccGraph |
Program dependency graph - only used for ASP-problems.
1.8.7