Clasp::WeightLitsRep Struct Reference

Primitive representation of weight constraint literals in normal form. More...

#include <weight_constraint.h>

Collaboration diagram for Clasp::WeightLitsRep:

Public Member Functions
bool	propagate (Solver &s, Literal W)
	Propagates the constraint W == *this. More...
bool	sat () const
bool	unsat () const
bool	open () const
bool	hasWeights () const

Static Public Member Functions
static WeightLitsRep	create (Solver &s, WeightLitVec &lits, weight_t bound)
	Transforms the given literals to the normal form expected by WeightConstraint. More...

Public Attributes
WeightLiteral *	lits
uint32	size
weight_t	bound
weight_t	reach

Detailed Description

Primitive representation of weight constraint literals in normal form.

Member Function Documentation

WeightLitsRep Clasp::WeightLitsRep::create ( Solver &  s, WeightLitVec &  lits, weight_t  bound  )

static

Transforms the given literals to the normal form expected by WeightConstraint.

The function simplifies lits and bound by removing assigned and merging duplicate/complementary literals. Furthermore, negative weights and their literals are inverted, bound is updated accordingly, and literals are sorted by decreasing weight.

Here is the call graph for this function:

bool Clasp::WeightLitsRep::hasWeights ( ) const

inline

bool Clasp::WeightLitsRep::open ( ) const

inline

bool Clasp::WeightLitsRep::propagate	(	Solver &	s,
		Literal	W
	)

Propagates the constraint W == *this.

If *this is always satisfied (bound <= 0) or unsatisfied (bound > reach), the function forward propagates W. Otherwise, if W is not free, it assigns (and removes) literals from *this that must hold.

Here is the call graph for this function:

bool Clasp::WeightLitsRep::sat ( ) const

inline

bool Clasp::WeightLitsRep::unsat ( ) const

inline

Member Data Documentation

weight_t Clasp::WeightLitsRep::bound

Rhs of linear constraint.

WeightLiteral* Clasp::WeightLitsRep::lits

Literals sorted by decreasing weight.

weight_t Clasp::WeightLitsRep::reach

Sum of weights of lits.

uint32 Clasp::WeightLitsRep::size

Number of literals in lits.

---

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

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