Clasp::Antecedent Class Reference

Stores a reference to the constraint that implied a literal. More...

#include <constraint.h>

Collaboration diagram for Clasp::Antecedent:

Public Types
enum	Type { generic_constraint = 0, ternary_constraint = 1, binary_constraint = 2 }

Public Member Functions
	Antecedent ()
	Creates a null Antecedent. More...
	Antecedent (const Literal &p)
	Creates an Antecedent from the literal p. More...
	Antecedent (const Literal &p, const Literal &q)
	Creates an Antecedent from the literals p and q. More...
	Antecedent (Constraint *con)
	Creates an Antecedent from the Constraint con. More...
bool	isNull () const
	Returns true if this antecedent does not refer to any constraint. More...
Type	type () const
	Returns the antecedent's type. More...
bool	learnt () const
	Returns true if the antecedent is a learnt nogood. More...
Constraint *	constraint () const
	Extracts the constraint-pointer stored in this object. More...
Literal	firstLiteral () const
	Extracts the first literal stored in this object. More...
Literal	secondLiteral () const
	Extracts the second literal stored in this object. More...
void	reason (Solver &s, Literal p, LitVec &lits) const
	Returns the reason for p. More...
template<class S >
bool	minimize (S &s, Literal p, CCMinRecursive *rec) const
bool	operator== (const Constraint *con) const
	Returns true iff the antecedent refers to the constraint con. More...
uint64	asUint () const
uint64 &	asUint ()

Static Public Member Functions
static bool	checkPlatformAssumptions ()
	Checks whether the imlementation-assumptions hold on this platform. More...

Detailed Description

Stores a reference to the constraint that implied a literal.

Stores a reference to the constraint that implied a certain literal or null if the literal has no antecedent (i.e. is a decision literal or a top-level fact).

Note

The constraint that implied a literal can have three different representations:

• it can be a single literal (binary clause constraint)
• it can be two literals (ternary clause constraint)
• it can be a pointer to a constraint (generic constraint)

Implementation:

The class stores all three representations in one 64-bit integer and makes the following platform assumptions:

• there is a 64-bit integer type
• pointers are either 32- or 64-bits wide.
• the alignment of pointers to dynamically allocated objects is a multiple of 4
• casting between 64-bit integers and pointers is safe and won't change the underlying value.

These assumptions are not guaranteed by the C++ Standard but should nontheless hold on most 32- and 64-bit platforms.

From the 64-bits the first 2-bits encode the type stored:

• 00: Pointer to constraint
• 01: ternary constraint (i.e. two literals stored in the remaining 62 bits).
• 10: binary constraint (i.e. one literal stored in the highest 31 bits)

Member Enumeration Documentation

enum Clasp::Antecedent::Type

Enumerator
generic_constraint
ternary_constraint
binary_constraint

Constructor & Destructor Documentation

Clasp::Antecedent::Antecedent ( )

inline

Creates a null Antecedent.

Postcondition

: isNull() == true && type == generic_constraint

Clasp::Antecedent::Antecedent ( const Literal &  p )

inline

Creates an Antecedent from the literal p.

Postcondition

: type() == binary_constraint && firstLiteral() == p

Here is the call graph for this function:

Clasp::Antecedent::Antecedent ( const Literal &  p, const Literal &  q  )

inline

Creates an Antecedent from the literals p and q.

Postcondition

type() == ternary_constraint && firstLiteral() == p && secondLiteral() == q

Here is the call graph for this function:

Clasp::Antecedent::Antecedent ( Constraint *  con )

inline

Creates an Antecedent from the Constraint con.

Postcondition

type() == generic_constraint && constraint() == con

Member Function Documentation

uint64 Clasp::Antecedent::asUint ( ) const

inline

uint64& Clasp::Antecedent::asUint ( )

inline

bool Clasp::Antecedent::checkPlatformAssumptions ( )

static

Checks whether the imlementation-assumptions hold on this platform.

throws PlatformError on error

Here is the call graph for this function:

Constraint* Clasp::Antecedent::constraint ( ) const

inline

Extracts the constraint-pointer stored in this object.

Precondition

type() == generic_constraint

Literal Clasp::Antecedent::firstLiteral ( ) const

inline

Extracts the first literal stored in this object.

Precondition

type() != generic_constraint

Here is the call graph for this function:

bool Clasp::Antecedent::isNull ( ) const

inline

Returns true if this antecedent does not refer to any constraint.

bool Clasp::Antecedent::learnt ( ) const

inline

Returns true if the antecedent is a learnt nogood.

template<class S >

bool Clasp::Antecedent::minimize ( S &  s, Literal  p, CCMinRecursive *  rec  ) const

inline

bool Clasp::Antecedent::operator== ( const Constraint *  con ) const

inline

Returns true iff the antecedent refers to the constraint con.

void Clasp::Antecedent::reason ( Solver &  s, Literal  p, LitVec &  lits  ) const

inline

Returns the reason for p.

Precondition

!isNull()

Literal Clasp::Antecedent::secondLiteral ( ) const

inline

Extracts the second literal stored in this object.

Precondition

type() == ternary_constraint

Here is the call graph for this function:

Type Clasp::Antecedent::type ( ) const

inline

Returns the antecedent's type.

---

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

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