Clasp::ClaspFacade::Result Struct Reference

Result of a solving step. More...

#include <clasp_facade.h>

Collaboration diagram for Clasp::ClaspFacade::Result:

Public Types
enum	Base { UNKNOWN = 0, SAT = 1, UNSAT = 2 }
	Possible solving results. More...
enum	Ext { EXT_EXHAUST = 4, EXT_INTERRUPT = 8, EXT_ERROR = 16 }

Public Member Functions
bool	sat () const
bool	unsat () const
bool	unknown () const
bool	exhausted () const
bool	interrupted () const
bool	error () const
	operator Base () const
	operator double () const

Public Attributes
uint8	flags
uint8	signal

Detailed Description

Result of a solving step.

Member Enumeration Documentation

enum Clasp::ClaspFacade::Result::Base

Possible solving results.

Enumerator
UNKNOWN	Satisfiability unknown - a given solve limit was hit.
SAT	Problem is satisfiable (a model was found).
UNSAT	Problem is unsatisfiable.

enum Clasp::ClaspFacade::Result::Ext

Enumerator
EXT_EXHAUST	Search space is exhausted.
EXT_INTERRUPT	The run was interrupted from outside.
EXT_ERROR	The run was terminated because of an internal error.

Member Function Documentation

bool Clasp::ClaspFacade::Result::error ( ) const

inline

bool Clasp::ClaspFacade::Result::exhausted ( ) const

inline

bool Clasp::ClaspFacade::Result::interrupted ( ) const

inline

Clasp::ClaspFacade::Result::operator Base ( ) const

inline

Clasp::ClaspFacade::Result::operator double ( ) const

inline

bool Clasp::ClaspFacade::Result::sat ( ) const

inline

bool Clasp::ClaspFacade::Result::unknown ( ) const

inline

bool Clasp::ClaspFacade::Result::unsat ( ) const

inline

Member Data Documentation

uint8 Clasp::ClaspFacade::Result::flags

uint8 Clasp::ClaspFacade::Result::signal

---

The documentation for this struct was generated from the following file:

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