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

#include <shared_context.h>

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
ImplicationList &	getList (Literal p)
ShortImplicationsGraph &	operator= (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

typedef bk_lib::left_right_sequence<Literal, std::pair<Literal,Literal>, 64> Clasp::ShortImplicationsGraph::ImplicationList [private]

Definition at line 305 of file shared_context.h.

typedef PodVector<ImplicationList>::type Clasp::ShortImplicationsGraph::ImpLists [private]

Definition at line 344 of file shared_context.h.

Member Enumeration Documentation

enum Clasp::ShortImplicationsGraph::ImpType

Enumerator:

binary_imp
ternary_imp

Definition at line 232 of file shared_context.h.

Constructor & Destructor Documentation

Clasp::ShortImplicationsGraph::ShortImplicationsGraph ( )

Definition at line 155 of file shared_context.cpp.

Clasp::ShortImplicationsGraph::~ShortImplicationsGraph ( )

Definition at line 160 of file shared_context.cpp.

Clasp::ShortImplicationsGraph::ShortImplicationsGraph ( const ShortImplicationsGraph & ) [private]

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.

ImplicationList& Clasp::ShortImplicationsGraph::getList ( Literal p ) [inline, private]

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.

uint32 Clasp::ShortImplicationsGraph::numEdges ( Literal p ) const

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]

bool Clasp::ShortImplicationsGraph::propagate	(	Solver &	s,
		Literal	p
	)		const

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.

void Clasp::ShortImplicationsGraph::remove_bin	(	ImplicationList &	w,
		Literal	p
	)		`[private]`

Definition at line 210 of file shared_context.cpp.

void Clasp::ShortImplicationsGraph::remove_tern	(	ImplicationList &	w,
		Literal	p
	)		`[private]`

Definition at line 214 of file shared_context.cpp.

void Clasp::ShortImplicationsGraph::removeTrue	(	const Solver &	s,
		Literal	p
	)

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

uint32 Clasp::ShortImplicationsGraph::bin_[2] [private]

Definition at line 346 of file shared_context.h.

ImpLists Clasp::ShortImplicationsGraph::graph_ [private]

Definition at line 345 of file shared_context.h.

bool Clasp::ShortImplicationsGraph::shared_ [private]

Definition at line 348 of file shared_context.h.

uint32 Clasp::ShortImplicationsGraph::tern_[2] [private]

Definition at line 347 of file shared_context.h.

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

Classes

Public Types

Public Member Functions

Private Types