Classes | Public Types | Public Member Functions | Private Types | Private Member Functions | Private Attributes
Clasp::ShortImplicationsGraph Class Reference

A class for efficiently storing and propagating binary and ternary clauses. More...

#include <shared_context.h>

List of all members.

Classes

struct  Propagate
struct  ReverseArc

Public Types

enum  ImpType { binary_imp = 2, ternary_imp = 3 }

Public Member Functions

bool add (ImpType t, bool learnt, const Literal *lits)
 Adds the given constraint to the implication graph.
template<class OP >
bool forEach (Literal p, const OP &op) const
 Applies op on all unary- and binary implications following from p.
void markShared (bool b)
 Mark the instance as shared/unshared.
uint32 numBinary () const
uint32 numEdges (Literal p) const
uint32 numLearnt () const
uint32 numTernary () const
bool propagate (Solver &s, Literal p) const
 Propagates consequences of p following from binary and ternary clauses.
bool propagateBin (Assignment &out, Literal p, uint32 dl) const
 Propagates immediate consequences of p following from binary clauses only.
void removeTrue (const Solver &s, Literal p)
 Removes p and its implications.
void resize (uint32 nodes)
 Makes room for nodes number of nodes.
bool reverseArc (const Solver &s, Literal p, uint32 maxLev, Antecedent &out) const
 Checks whether there is a reverse arc implying p and if so returns it in out.
 ShortImplicationsGraph ()
uint32 size () const
 ~ShortImplicationsGraph ()

Private Types

typedef
bk_lib::left_right_sequence
< Literal, std::pair< Literal,
Literal >, 64 > 
ImplicationList
typedef PodVector
< ImplicationList >::type 
ImpLists

Private Member Functions

ImplicationListgetList (Literal p)
ShortImplicationsGraphoperator= (ShortImplicationsGraph &)
void remove_bin (ImplicationList &w, Literal p)
void remove_tern (ImplicationList &w, Literal p)
 ShortImplicationsGraph (const ShortImplicationsGraph &)

Private Attributes

uint32 bin_ [2]
ImpLists graph_
bool shared_
uint32 tern_ [2]

Detailed Description

A class for efficiently storing and propagating binary and ternary clauses.

Definition at line 228 of file shared_context.h.


Member Typedef Documentation

Definition at line 305 of file shared_context.h.

Definition at line 344 of file shared_context.h.


Member Enumeration Documentation

Enumerator:
binary_imp 
ternary_imp 

Definition at line 232 of file shared_context.h.


Constructor & Destructor Documentation

Definition at line 155 of file shared_context.cpp.

Definition at line 160 of file shared_context.cpp.


Member Function Documentation

bool Clasp::ShortImplicationsGraph::add ( ImpType  t,
bool  learnt,
const Literal lits 
)

Adds the given constraint to the implication graph.

Returns:
true iff a new implication was added.

Definition at line 178 of file shared_context.cpp.

template<class OP >
bool Clasp::ShortImplicationsGraph::forEach ( Literal  p,
const OP &  op 
) const [inline]

Applies op on all unary- and binary implications following from p.

OP must provide two functions:

  • bool unary(Literal, Literal)
  • bool binary(Literal, Literal, Literal) The first argument will be p, the second (resp. third) the unary (resp. binary) clause implied by p.
    Note:
    For learnt imps, at least one literal has its watch-flag set.

Definition at line 279 of file shared_context.h.

Definition at line 341 of file shared_context.h.

void Clasp::ShortImplicationsGraph::markShared ( bool  b) [inline]

Mark the instance as shared/unshared.

A shared instance adds learnt binary/ternary clauses to specialized shared blocks of memory.

Definition at line 241 of file shared_context.h.

uint32 Clasp::ShortImplicationsGraph::numBinary ( ) const [inline]

Definition at line 264 of file shared_context.h.

Definition at line 176 of file shared_context.cpp.

uint32 Clasp::ShortImplicationsGraph::numLearnt ( ) const [inline]

Definition at line 266 of file shared_context.h.

uint32 Clasp::ShortImplicationsGraph::numTernary ( ) const [inline]

Definition at line 265 of file shared_context.h.

ShortImplicationsGraph& Clasp::ShortImplicationsGraph::operator= ( ShortImplicationsGraph ) [private]

Propagates consequences of p following from binary and ternary clauses.

Precondition:
s.isTrue(p)

Definition at line 298 of file shared_context.cpp.

bool Clasp::ShortImplicationsGraph::propagateBin ( Assignment out,
Literal  p,
uint32  dl 
) const

Propagates immediate consequences of p following from binary clauses only.

Definition at line 300 of file shared_context.cpp.

Definition at line 210 of file shared_context.cpp.

Definition at line 214 of file shared_context.cpp.

Removes p and its implications.

Precondition:
s.isTrue(p)

Definition at line 228 of file shared_context.cpp.

void Clasp::ShortImplicationsGraph::resize ( uint32  nodes)

Makes room for nodes number of nodes.

Definition at line 163 of file shared_context.cpp.

bool Clasp::ShortImplicationsGraph::reverseArc ( const Solver s,
Literal  p,
uint32  maxLev,
Antecedent out 
) const

Checks whether there is a reverse arc implying p and if so returns it in out.

Definition at line 299 of file shared_context.cpp.

uint32 Clasp::ShortImplicationsGraph::size ( ) const [inline]

Definition at line 268 of file shared_context.h.


Member Data Documentation

Definition at line 346 of file shared_context.h.

Definition at line 345 of file shared_context.h.

Definition at line 348 of file shared_context.h.

Definition at line 347 of file shared_context.h.


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


clasp
Author(s): Benjamin Kaufmann
autogenerated on Thu Aug 27 2015 12:41:41