Provides a simplified interface to the services of the clasp library. More...

#include <clasp_facade.h>

Inheritance diagram for Clasp::ClaspFacade:

Collaboration diagram for Clasp::ClaspFacade:

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 ()

	~ClaspFacade ()

Result	solve (Clasp::EventHandler *onModel=0)
	Solves the current prepared problem. More...

bool	ok () const
	Returns whether the problem is still valid. More...

bool	terminate (int signal)
	Tries to terminate an active solve operation. More...

const Summary &	shutdown ()

bool	solving () const
	Returns whether a solve operation is currently active. More...

const Summary &	summary () const
	Returns the summary of the active step. More...

const ClaspConfig *	config () const
	Returns the active configuration. More...

int	step () const
	Returns the current incremental step (starts at 0). More...

Result	result () const
	Returns the result of the active step. (unknown if run is not yet completed). More...

ProgramBuilder *	program () const
	Returns the active program or 0 if it was already released. More...

ExpectedQuantity	getStat (const char *path) const

const char *	getKeys (const char *path) const

Public Member Functions inherited from Clasp::EventHandler
	EventHandler (Event::Verbosity verbosity=Event::verbosity_quiet)

virtual	~EventHandler ()

void	setVerbosity (Event::Subsystem sys, Event::Verbosity verb)

void	dispatch (const Event &ev)

virtual void	onEvent (const Event &)

Public Attributes
SharedContext	ctx

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. More...

SatBuilder &	startSat (ClaspConfig &config, bool allowUpdate=false)
	Starts definition of a SAT-problem. More...

PBBuilder &	startPB (ClaspConfig &config, bool allowUpdate=false)
	Starts definition of a PB-problem. More...

ProgramBuilder &	start (ClaspConfig &config, ProblemType t, bool allowUpdate=false)
	Starts definition of a problem of type t. More...

bool	prepare (EnumMode m=enum_volatile)
	Finishes the definition of a problem and prepares it for solving. More...

void	assume (Literal p)
	Adds p to the list of assumptions under which solving should operate. More...

void	assume (const LitVec &ext)
	Calls assume(p) for all literals p in ext. More...

ProgramBuilder &	update (bool updateConfig=false)
	Starts update of the active problem. More...

Detailed Description

Provides a simplified interface to the services of the clasp library.

Member Enumeration Documentation

enum Clasp::ClaspFacade::EnumMode

Enumerator
enum_volatile
enum_static

Constructor & Destructor Documentation

Clasp::ClaspFacade::ClaspFacade ( )

Clasp::ClaspFacade::~ClaspFacade ( )

Member Function Documentation

void Clasp::ClaspFacade::assume ( Literal p )

Adds p to the list of assumptions under which solving should operate.

void Clasp::ClaspFacade::assume ( const LitVec & ext )

Calls assume(p) for all literals p in ext.

const ClaspConfig* Clasp::ClaspFacade::config ( ) const

inline

Returns the active configuration.

const char * Clasp::ClaspFacade::getKeys ( const char * path ) const

Here is the call graph for this function:

ExpectedQuantity Clasp::ClaspFacade::getStat ( const char * path ) const

bool Clasp::ClaspFacade::ok ( ) const

inline

Returns whether the problem is still valid.

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.

Here is the call graph for this function:

ProgramBuilder* Clasp::ClaspFacade::program ( ) const

inline

Returns the active program or 0 if it was already released.

Here is the call graph for this function:

Result Clasp::ClaspFacade::result ( ) const

inline

Returns the result of the active step. (unknown if run is not yet completed).

const ClaspFacade::Summary & Clasp::ClaspFacade::shutdown ( )

Here is the call graph for this function:

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.

Here is the call graph for this function:

bool Clasp::ClaspFacade::solving ( ) const

Returns whether a solve operation is currently active.

Here is the call graph for this function:

ProgramBuilder & Clasp::ClaspFacade::start	(	ClaspConfig &	config,
		ProblemType	t,
		bool	allowUpdate = `false`
	)

Starts definition of a problem of type t.

Here is the call graph for this function:

Asp::LogicProgram & Clasp::ClaspFacade::startAsp	(	ClaspConfig &	config,
		bool	allowUpdate = `false`
	)

Starts definition of an ASP-problem.

Here is the call graph for this function:

PBBuilder & Clasp::ClaspFacade::startPB	(	ClaspConfig &	config,
		bool	allowUpdate = `false`
	)

Starts definition of a PB-problem.

Here is the call graph for this function:

SatBuilder & Clasp::ClaspFacade::startSat	(	ClaspConfig &	config,
		bool	allowUpdate = `false`
	)

Starts definition of a SAT-problem.

Here is the call graph for this function:

int Clasp::ClaspFacade::step ( ) const

inline

Returns the current incremental step (starts at 0).

const Summary& Clasp::ClaspFacade::summary ( ) const

inline

Returns the summary of the active step.

bool Clasp::ClaspFacade::terminate ( int signal )

Tries to terminate an active solve operation.

Here is the call graph for this function:

ProgramBuilder & Clasp::ClaspFacade::update ( bool updateConfig = false )

Starts update of the active problem.

Precondition: start() was called with allowUpdate and solving() is false.

Here is the call graph for this function:

Member Data Documentation

SharedContext Clasp::ClaspFacade::ctx

Context-object used to store problem.

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

/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/clasp_facade.h
/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/clasp_facade.cpp

Classes

Public Member Functions

Public Attributes

Start functions

Detailed Description

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation