#include <solver_types.h>
Public Types | |
enum | { MAX_LBD = Activity::MAX_LBD, MAX_ACTIVITY = (1<<21)-1 } |
typedef ClauseInfo | self_type |
Public Member Functions | |
uint32 | activity () const |
bool | aux () const |
ClauseInfo (ConstraintType t=Constraint_t::static_constraint) | |
uint32 | lbd () const |
bool | learnt () const |
self_type & | setActivity (uint32 act) |
self_type & | setAux (bool b) |
self_type & | setLbd (uint32 a_lbd) |
self_type & | setTagged (bool b) |
self_type & | setType (ConstraintType t) |
bool | tagged () const |
ConstraintType | type () const |
Private Attributes | |
uint32 | act_: 21 |
uint32 | aux_: 1 |
uint32 | lbd_: 7 |
uint32 | tag_: 1 |
uint32 | type_: 2 |
Type storing initial information on a (learnt) clause.
Definition at line 362 of file solver_types.h.
Definition at line 364 of file solver_types.h.
anonymous enum |
Definition at line 365 of file solver_types.h.
Definition at line 366 of file solver_types.h.
uint32 Clasp::ClauseInfo::activity | ( | ) | const [inline] |
Definition at line 371 of file solver_types.h.
bool Clasp::ClauseInfo::aux | ( | ) | const [inline] |
Definition at line 374 of file solver_types.h.
uint32 Clasp::ClauseInfo::lbd | ( | ) | const [inline] |
Definition at line 372 of file solver_types.h.
bool Clasp::ClauseInfo::learnt | ( | ) | const [inline] |
Definition at line 369 of file solver_types.h.
self_type& Clasp::ClauseInfo::setActivity | ( | uint32 | act | ) | [inline] |
Definition at line 376 of file solver_types.h.
self_type& Clasp::ClauseInfo::setAux | ( | bool | b | ) | [inline] |
Definition at line 379 of file solver_types.h.
self_type& Clasp::ClauseInfo::setLbd | ( | uint32 | a_lbd | ) | [inline] |
Definition at line 378 of file solver_types.h.
self_type& Clasp::ClauseInfo::setTagged | ( | bool | b | ) | [inline] |
Definition at line 377 of file solver_types.h.
self_type& Clasp::ClauseInfo::setType | ( | ConstraintType | t | ) | [inline] |
Definition at line 375 of file solver_types.h.
bool Clasp::ClauseInfo::tagged | ( | ) | const [inline] |
Definition at line 373 of file solver_types.h.
ConstraintType Clasp::ClauseInfo::type | ( | ) | const [inline] |
Definition at line 370 of file solver_types.h.
uint32 Clasp::ClauseInfo::act_ [private] |
Definition at line 381 of file solver_types.h.
uint32 Clasp::ClauseInfo::aux_ [private] |
Definition at line 385 of file solver_types.h.
uint32 Clasp::ClauseInfo::lbd_ [private] |
Definition at line 382 of file solver_types.h.
uint32 Clasp::ClauseInfo::tag_ [private] |
Definition at line 384 of file solver_types.h.
uint32 Clasp::ClauseInfo::type_ [private] |
Definition at line 383 of file solver_types.h.