#include <clasp/literal.h>
#include <clasp/constraint.h>
#include <clasp/util/left_right_sequence.h>
#include <clasp/util/misc_types.h>
#include <clasp/util/type_manip.h>
#include <numeric>

Include dependency graph for solver_types.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	Clasp::Assignment
	Stores assignment related information. More...
struct	Clasp::SmallClauseAlloc::Block
struct	Clasp::CCMinRecursive
struct	Clasp::SmallClauseAlloc::Chunk
class	Clasp::ClauseHead
	(Abstract) base class for clause types. More...
class	Clasp::ClauseInfo
struct	Clasp::ClauseRep
	Primitive representation of a clause. More...
struct	Clasp::ClauseWatch
struct	Clasp::CoreStats
	A struct for holding core statistics used by a solver. More...
union	Clasp::ClauseHead::Data
struct	Clasp::GenericWatch::EqConstraint
struct	Clasp::ClauseWatch::EqHead
struct	Clasp::ExtendedStats
	A struct for holding (optional) extra statistics. More...
struct	Clasp::GenericWatch
	Represents a generic watch in a Solver. More...
struct	Clasp::ImpliedList
	A type for storing ImpliedLiteral objects. More...
struct	Clasp::ImpliedLiteral
	Stores information about a literal that is implied on an earlier level than the current decision level. More...
union	Clasp::ClauseHead::Info
struct	Clasp::JumpStats
	A struct for holding (optional) jump statistics. More...
struct	Clasp::ClauseHead::Data::LocalClause
struct	Clasp::QueueImpl
struct	Clasp::ReasonStore32
struct	Clasp::ReasonStore64
	Type for storing reasons for variable assignments together with additional data. More...
class	Clasp::SmallClauseAlloc
	Allocator for small (at most 32-byte) clauses. More...
struct	Clasp::SolverStats
	A struct for aggregating statistics maintained in a solver object. More...
struct	Clasp::SumQueue
struct	Clasp::ReasonStore64::value_type
struct	Clasp::ReasonStore32::value_type
struct	Clasp::ValueSet
	A set of configurable values for a variable. More...
Namespaces
namespace	Clasp
Defines
#define	CLASP_CORE_STATS(STAT, SELF, OTHER)
#define	CLASP_EXTENDED_STATS(STAT, SELF, OTHER)
#define	CLASP_JUMP_STATS(STAT, SELF, OTHER)
#define	CLASP_STAT_ACCU(m, k, a, accu) accu;
#define	CLASP_STAT_DEFINE(m, k, a, accu) m
#define	CLASP_STAT_GET(m, k, a, accu) if (std::strcmp(key, k) == 0) { return double( (a) ); }
#define	CLASP_STAT_KEY(m, k, a, accu) k "\0"
#define	MAX_MEM(X, Y) X = std::max((X), (Y))
#define	NO_ARG
Typedefs
typedef bk_lib::left_right_sequence < ClauseWatch, GenericWatch, 0 >	Clasp::WatchList
	Watch list type.
Functions
bool	Clasp::matchStatPath (const char &x, const char path, std::size_t len)
bool	Clasp::matchStatPath (const char &x, const char path)
double	Clasp::percent (uint64 x, uint64 y)
double	Clasp::ratio (uint64 x, uint64 y)
void	Clasp::releaseVec (WatchList &w)

Detailed Description

Contains some types used by a Solver

Definition in file solver_types.h.

Define Documentation

#define CLASP_CORE_STATS	(	STAT,
		SELF,
		OTHER
	)

Value:

STAT(uint64 choices;    , STRING(choices)    , SELF.choices    , SELF.choices    += OTHER.choices   )\
        STAT(uint64 conflicts;  , STRING(conflicts)  , SELF.conflicts  , SELF.conflicts  += OTHER.conflicts )\
        STAT(uint64 analyzed;   , STRING(analyzed)   , SELF.analyzed   , SELF.analyzed   += OTHER.analyzed  )\
        STAT(uint64 restarts;   , STRING(restarts)   , SELF.restarts   , SELF.restarts   += OTHER.restarts  )\
        STAT(uint64 lastRestart;, STRING(lastRestart), SELF.lastRestart, SELF.lastRestart = std::max(SELF.lastRestart, OTHER.lastRestart))

Definition at line 72 of file solver_types.h.

#define CLASP_EXTENDED_STATS	(	STAT,
		SELF,
		OTHER
	)

Value:

STAT(uint64 domChoices; , STRING(domChoices) , SELF.domChoices , SELF.domChoices += OTHER.domChoices) \
        STAT(uint64 models;     , STRING(models)     , SELF.models     , SELF.models     += OTHER.models)     \
        STAT(uint64 modelLits;  , STRING(modelLits)  , SELF.modelLits  , SELF.modelLits  += OTHER.modelLits)  \
        STAT(uint64 hccTests;   , STRING(hccTests)   , SELF.hccTests   , SELF.hccTests   += OTHER.hccTests)   \
        STAT(uint64 hccPartial; , STRING(hccPartial) , SELF.hccPartial , SELF.hccPartial += OTHER.hccPartial) \
        STAT(uint64 deleted;    , STRING(deleted)    , SELF.deleted    , SELF.deleted    += OTHER.deleted)    \
        STAT(uint64 distributed;, STRING(distributed), SELF.distributed, SELF.distributed+= OTHER.distributed)\
        STAT(uint64 sumDistLbd; , STRING(sumDistLbd) , SELF.sumDistLbd , SELF.sumDistLbd += OTHER.sumDistLbd) \
        STAT(uint64 integrated; , STRING(integrated) , SELF.integrated , SELF.integrated += OTHER.integrated) \
        STAT(Array learnts;  , "lemmas"           , SELF.lemmas()   , NO_ARG)   \
        STAT(Array lits;     , "learntLits"       , SELF.learntLits(), NO_ARG)  \
        STAT(uint32 binary;  , STRING(binary)     , SELF.binary  , SELF.binary  += OTHER.binary)  \
        STAT(uint32 ternary; , STRING(ternary)    , SELF.ternary , SELF.ternary += OTHER.ternary) \
        STAT(double cpuTime; , STRING(cpuTime)    , SELF.cpuTime , SELF.cpuTime += OTHER.cpuTime) \
        STAT(uint64 intImps; , STRING(intImps)    , SELF.intImps , SELF.intImps+= OTHER.intImps)  \
        STAT(uint64 intJumps; , STRING(intJumps)   , SELF.intJumps, SELF.intJumps+=OTHER.intJumps) \
        STAT(uint64 gpLits;  , STRING(gpLits)     , SELF.gpLits  , SELF.gpLits  += OTHER.gpLits)  \
        STAT(uint32 gps;     , STRING(gps)        , SELF.gps     , SELF.gps     += OTHER.gps)     \
        STAT(uint32 splits;  , STRING(splits)     , SELF.splits  , SELF.splits  += OTHER.splits)  \
        STAT(NO_ARG       , "conflictLemmas", SELF.lemmas(Constraint_t::learnt_conflict), SELF.learnts[0] += OTHER.learnts[0]) \
        STAT(NO_ARG       , "loopLemmas"    , SELF.lemmas(Constraint_t::learnt_loop)    , SELF.learnts[1] += OTHER.learnts[1]) \
        STAT(NO_ARG       , "otherLemmas"   , SELF.lemmas(Constraint_t::learnt_other)   , SELF.learnts[2] += OTHER.learnts[2]) \
        STAT(NO_ARG       , "conflictLits"  , SELF.lits[Constraint_t::learnt_conflict-1], SELF.lits[0]    += OTHER.lits[0])    \
        STAT(NO_ARG       , "loopLits"      , SELF.lits[Constraint_t::learnt_loop-1]    , SELF.lits[1]    += OTHER.lits[1])    \
        STAT(NO_ARG       , "otherLits"     , SELF.lits[Constraint_t::learnt_other-1]   , SELF.lits[2]    += OTHER.lits[2])

Definition at line 102 of file solver_types.h.

#define CLASP_JUMP_STATS	(	STAT,
		SELF,
		OTHER
	)

Value:

STAT(uint64 jumps;    , STRING(jumps)    , SELF.jumps    , SELF.jumps    += OTHER.jumps)   \
        STAT(uint64 bounded;  , STRING(bounded)  , SELF.bounded  , SELF.bounded  += OTHER.bounded)  \
        STAT(uint64 jumpSum;  , STRING(jumpSum)  , SELF.jumpSum  , SELF.jumpSum  += OTHER.jumpSum)  \
        STAT(uint64 boundSum; , STRING(boundSum) , SELF.boundSum , SELF.boundSum += OTHER.boundSum) \
        STAT(uint32 maxJump;  , STRING(maxJump)  , SELF.maxJump  , MAX_MEM(SELF.maxJump, OTHER.maxJump))   \
        STAT(uint32 maxJumpEx;, STRING(maxJumpEx), SELF.maxJumpEx, MAX_MEM(SELF.maxJumpEx,OTHER.maxJumpEx)) \
        STAT(uint32 maxBound; , STRING(maxBound) , SELF.maxBound , MAX_MEM(SELF.maxBound, OTHER.maxBound))

Definition at line 164 of file solver_types.h.

#define MAX_MEM	(	X,
		Y
	)	X = std::max((X), (Y))

Classes

Namespaces

Defines

Typedefs

Functions

Detailed Description

Define Documentation