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

#include <shared_context.h>

Collaboration diagram for Clasp::ShortImplicationsGraph:

Classes
struct	Propagate

struct	ReverseArc

Public Types
enum	ImpType { binary_imp = 2, ternary_imp = 3 }

Public Member Functions
	ShortImplicationsGraph ()

	~ShortImplicationsGraph ()

void	resize (uint32 nodes)
	Makes room for nodes number of nodes. More...

void	markShared (bool b)
	Mark the instance as shared/unshared. More...

bool	add (ImpType t, bool learnt, const Literal *lits)
	Adds the given constraint to the implication graph. More...

void	removeTrue (const Solver &s, Literal p)
	Removes p and its implications. More...

bool	propagate (Solver &s, Literal p) const
	Propagates consequences of p following from binary and ternary clauses. More...

bool	propagateBin (Assignment &out, Literal p, uint32 dl) const
	Propagates immediate consequences of p following from binary clauses only. More...

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. More...

uint32	numBinary () const

uint32	numTernary () const

uint32	numLearnt () const

uint32	numEdges (Literal p) const

uint32	size () const

template<class OP >
bool	forEach (Literal p, const OP &op) const
	Applies op on all unary- and binary implications following from p. More...

Detailed Description

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

Member Enumeration Documentation

enum Clasp::ShortImplicationsGraph::ImpType

Enumerator
binary_imp
ternary_imp

Constructor & Destructor Documentation

Clasp::ShortImplicationsGraph::ShortImplicationsGraph ( )

Clasp::ShortImplicationsGraph::~ShortImplicationsGraph ( )

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.

Here is the call graph for this function:

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.

Here is the call graph for this function:

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.

uint32 Clasp::ShortImplicationsGraph::numBinary ( ) const

inline

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

Here is the call graph for this function:

uint32 Clasp::ShortImplicationsGraph::numLearnt ( ) const

inline

uint32 Clasp::ShortImplicationsGraph::numTernary ( ) const

inline

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

Propagates consequences of p following from binary and ternary clauses.

Precondition: s.isTrue(p)

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

Propagates immediate consequences of p following from binary clauses only.

Here is the call graph for this function:

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

Removes p and its implications.

Precondition: s.isTrue(p)

Here is the call graph for this function:

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

Makes room for nodes number of nodes.

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.

uint32 Clasp::ShortImplicationsGraph::size ( ) const

inline

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

/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/shared_context.h
/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/shared_context.cpp

Classes

Public Types

Public Member Functions

Detailed Description

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation