Provides a simplified interface to the services of the clasp library. More...
#include <clasp_facade.h>
Classes | |
| struct | Result |
| Result of a solving step. More... | |
| struct | SolveImpl |
| struct | SolveStrategy |
| struct | StepReady |
| Event type used to signal that a solve step has terminated. More... | |
| struct | StepStart |
| Event type used to signal that a solve step has started. More... | |
| struct | Summary |
| Type summarizing one or more solving steps. More... | |
Public Member Functions | |
| ClaspFacade () | |
| const ClaspConfig * | config () const |
| Returns the active configuration. | |
| const char * | getKeys (const char *path) const |
| ExpectedQuantity | getStat (const char *path) const |
| bool | ok () const |
| Returns whether the problem is still valid. | |
| ProgramBuilder * | program () const |
| Returns the active program or 0 if it was already released. | |
| Result | result () const |
| Returns the result of the active step. (unknown if run is not yet completed). | |
| const Summary & | shutdown () |
| Result | solve (Clasp::EventHandler *onModel=0) |
| Solves the current prepared problem. | |
| bool | solving () const |
| Returns whether a solve operation is currently active. | |
| int | step () const |
| Returns the current incremental step (starts at 0). | |
| const Summary & | summary () const |
| Returns the summary of the active step. | |
| bool | terminate (int signal) |
| Tries to terminate an active solve operation. | |
| ~ClaspFacade () | |
Public Attributes | |
| SharedContext | ctx |
Private Types | |
| typedef SingleOwnerPtr < ProgramBuilder > | BuilderPtr |
| typedef SingleOwnerPtr < Asp::LpStats > | LpStatsPtr |
| typedef SingleOwnerPtr< SolveImpl > | SolvePtr |
| typedef SingleOwnerPtr< Summary > | SummaryPtr |
Private Member Functions | |
| void | accuStep () |
| void | discardProblem () |
| ExpectedQuantity | getStat (const SharedContext &ctx, const char *key, bool accu, const Range< uint32 > &r) const |
| ExpectedQuantity | getStatImpl (const char *path, bool keys) const |
| void | init (ClaspConfig &cfg, bool discardProblem) |
| void | initBuilder (ProgramBuilder *in, bool incremental) |
| bool | onModel (const Solver &s, const Model &m) |
| void | startStep (uint32 num) |
| Result | stopStep (int signal, bool complete) |
Private Attributes | |
| SummaryPtr | accu_ |
| LitVec | assume_ |
| BuilderPtr | builder_ |
| ClaspConfig * | config_ |
| LpStatsPtr | lpStats_ |
| SolvePtr | solve_ |
| Summary | step_ |
Start functions | |
Functions for defining a problem. Calling one of the start functions discards any previous problem. The allowUpdate parameter determines whether or not program updates are allowed once the problem is initially defined. | |
| enum | EnumMode { enum_volatile, enum_static } |
| Asp::LogicProgram & | startAsp (ClaspConfig &config, bool allowUpdate=false) |
| Starts definition of an ASP-problem. | |
| SatBuilder & | startSat (ClaspConfig &config, bool allowUpdate=false) |
| Starts definition of a SAT-problem. | |
| PBBuilder & | startPB (ClaspConfig &config, bool allowUpdate=false) |
| Starts definition of a PB-problem. | |
| ProgramBuilder & | start (ClaspConfig &config, ProblemType t, bool allowUpdate=false) |
| Starts definition of a problem of type t. | |
| bool | prepare (EnumMode m=enum_volatile) |
| Finishes the definition of a problem and prepares it for solving. | |
| void | assume (Literal p) |
| Adds p to the list of assumptions under which solving should operate. | |
| void | assume (const LitVec &ext) |
| Calls assume(p) for all literals p in ext. | |
| ProgramBuilder & | update (bool updateConfig=false) |
| Starts update of the active problem. | |
Detailed Description
Provides a simplified interface to the services of the clasp library.
Definition at line 107 of file clasp_facade.h.
Member Typedef Documentation
typedef SingleOwnerPtr<ProgramBuilder> Clasp::ClaspFacade::BuilderPtr [private] |
Definition at line 312 of file clasp_facade.h.
typedef SingleOwnerPtr<Asp::LpStats> Clasp::ClaspFacade::LpStatsPtr [private] |
Definition at line 313 of file clasp_facade.h.
typedef SingleOwnerPtr<SolveImpl> Clasp::ClaspFacade::SolvePtr [private] |
Definition at line 314 of file clasp_facade.h.
typedef SingleOwnerPtr<Summary> Clasp::ClaspFacade::SummaryPtr [private] |
Definition at line 315 of file clasp_facade.h.
Member Enumeration Documentation
Definition at line 193 of file clasp_facade.h.
Constructor & Destructor Documentation
Definition at line 274 of file clasp_facade.cpp.
Definition at line 275 of file clasp_facade.cpp.
Member Function Documentation
| void Clasp::ClaspFacade::accuStep | ( | ) | [private] |
Definition at line 452 of file clasp_facade.cpp.
| void Clasp::ClaspFacade::assume | ( | Literal | p | ) |
Adds p to the list of assumptions under which solving should operate.
Definition at line 388 of file clasp_facade.cpp.
| void Clasp::ClaspFacade::assume | ( | const LitVec & | ext | ) |
Calls assume(p) for all literals p in ext.
Definition at line 391 of file clasp_facade.cpp.
| const ClaspConfig* Clasp::ClaspFacade::config | ( | ) | const [inline] |
Returns the active configuration.
Definition at line 301 of file clasp_facade.h.
| void Clasp::ClaspFacade::discardProblem | ( | ) | [private] |
Definition at line 276 of file clasp_facade.cpp.
| const char * Clasp::ClaspFacade::getKeys | ( | const char * | path | ) | const |
Definition at line 567 of file clasp_facade.cpp.
| ExpectedQuantity Clasp::ClaspFacade::getStat | ( | const char * | path | ) | const |
Definition at line 564 of file clasp_facade.cpp.
| ExpectedQuantity Clasp::ClaspFacade::getStat | ( | const SharedContext & | ctx, |
| const char * | key, | ||
| bool | accu, | ||
| const Range< uint32 > & | r | ||
| ) | const [private] |
Definition at line 572 of file clasp_facade.cpp.
| ExpectedQuantity Clasp::ClaspFacade::getStatImpl | ( | const char * | path, |
| bool | keys | ||
| ) | const [private] |
Definition at line 479 of file clasp_facade.cpp.
| void Clasp::ClaspFacade::init | ( | ClaspConfig & | cfg, |
| bool | discardProblem | ||
| ) | [private] |
Definition at line 285 of file clasp_facade.cpp.
| void Clasp::ClaspFacade::initBuilder | ( | ProgramBuilder * | in, |
| bool | incremental | ||
| ) | [private] |
Definition at line 302 of file clasp_facade.cpp.
| bool Clasp::ClaspFacade::ok | ( | ) | const [inline] |
Returns whether the problem is still valid.
Definition at line 292 of file clasp_facade.h.
| bool Clasp::ClaspFacade::onModel | ( | const Solver & | s, |
| const Model & | m | ||
| ) | [private, virtual] |
Reimplemented from Clasp::EventHandler.
Definition at line 466 of file clasp_facade.cpp.
| bool Clasp::ClaspFacade::prepare | ( | EnumMode | m = enum_volatile | ) |
Finishes the definition of a problem and prepares it for solving.
Once the problem is prepared, call solve() to solve it.
- Parameters:
-
m Mode to be used for all enumeration-related knowledge. If m is enum_volatile, all enumeration knowledge is learnt under an assumption that is retracted on program update. Otherwise, no special assumption is used and enumeration-related knowledge might become unretractable.
Definition at line 366 of file clasp_facade.cpp.
| ProgramBuilder* Clasp::ClaspFacade::program | ( | ) | const [inline] |
Returns the active program or 0 if it was already released.
Definition at line 307 of file clasp_facade.h.
| Result Clasp::ClaspFacade::result | ( | ) | const [inline] |
Returns the result of the active step. (unknown if run is not yet completed).
Definition at line 305 of file clasp_facade.h.
| const ClaspFacade::Summary & Clasp::ClaspFacade::shutdown | ( | ) |
Definition at line 396 of file clasp_facade.cpp.
| ClaspFacade::Result Clasp::ClaspFacade::solve | ( | Clasp::EventHandler * | onModel = 0 | ) |
Solves the current prepared problem.
- Precondition:
- !solving()
- Parameters:
-
handler An optional event handler that is notified on each model and once after the solve operation has completed.
- Note:
- If ok() is false or result().unsat() is true prior to calling solve(), i.e. the current step is already complete, the solve operation is not started and no events are generated.
Definition at line 403 of file clasp_facade.cpp.
| bool Clasp::ClaspFacade::solving | ( | ) | const |
Returns whether a solve operation is currently active.
Definition at line 394 of file clasp_facade.cpp.
| ProgramBuilder & Clasp::ClaspFacade::start | ( | ClaspConfig & | config, |
| ProblemType | t, | ||
| bool | allowUpdate = false |
||
| ) |
Starts definition of a problem of type t.
Definition at line 316 of file clasp_facade.cpp.
| Asp::LogicProgram & Clasp::ClaspFacade::startAsp | ( | ClaspConfig & | config, |
| bool | allowUpdate = false |
||
| ) |
Starts definition of an ASP-problem.
Definition at line 335 of file clasp_facade.cpp.
| PBBuilder & Clasp::ClaspFacade::startPB | ( | ClaspConfig & | config, |
| bool | allowUpdate = false |
||
| ) |
Starts definition of a PB-problem.
Definition at line 329 of file clasp_facade.cpp.
| SatBuilder & Clasp::ClaspFacade::startSat | ( | ClaspConfig & | config, |
| bool | allowUpdate = false |
||
| ) |
Starts definition of a SAT-problem.
Definition at line 323 of file clasp_facade.cpp.
| void Clasp::ClaspFacade::startStep | ( | uint32 | num | ) | [private] |
Definition at line 426 of file clasp_facade.cpp.
| int Clasp::ClaspFacade::step | ( | ) | const [inline] |
Returns the current incremental step (starts at 0).
Definition at line 303 of file clasp_facade.h.
| ClaspFacade::Result Clasp::ClaspFacade::stopStep | ( | int | signal, |
| bool | complete | ||
| ) | [private] |
Definition at line 433 of file clasp_facade.cpp.
| const Summary& Clasp::ClaspFacade::summary | ( | ) | const [inline] |
Returns the summary of the active step.
Definition at line 299 of file clasp_facade.h.
| bool Clasp::ClaspFacade::terminate | ( | int | signal | ) |
Tries to terminate an active solve operation.
Definition at line 357 of file clasp_facade.cpp.
| ProgramBuilder & Clasp::ClaspFacade::update | ( | bool | updateConfig = false | ) |
Starts update of the active problem.
Definition at line 345 of file clasp_facade.cpp.
Member Data Documentation
SummaryPtr Clasp::ClaspFacade::accu_ [private] |
Definition at line 329 of file clasp_facade.h.
LitVec Clasp::ClaspFacade::assume_ [private] |
Definition at line 330 of file clasp_facade.h.
BuilderPtr Clasp::ClaspFacade::builder_ [private] |
Definition at line 326 of file clasp_facade.h.
ClaspConfig* Clasp::ClaspFacade::config_ [private] |
Definition at line 325 of file clasp_facade.h.
Context-object used to store problem.
Definition at line 174 of file clasp_facade.h.
LpStatsPtr Clasp::ClaspFacade::lpStats_ [private] |
Definition at line 327 of file clasp_facade.h.
SolvePtr Clasp::ClaspFacade::solve_ [private] |
Definition at line 328 of file clasp_facade.h.
Summary Clasp::ClaspFacade::step_ [private] |
Definition at line 331 of file clasp_facade.h.
The documentation for this class was generated from the following files: