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

#include <weight_constraint.h>

Public Member Functions
bool	hasWeights () const
bool	open () const
bool	propagate (Solver &s, Literal W)
	Propagates the constraint W == *this.
bool	sat () const
bool	unsat () 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.
Public Attributes
weight_t	bound
WeightLiteral *	lits
weight_t	reach
uint32	size

Detailed Description

Primitive representation of weight constraint literals in normal form.

Definition at line 33 of file weight_constraint.h.

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.

Definition at line 34 of file weight_constraint.cpp.

bool Clasp::WeightLitsRep::hasWeights ( ) const [inline]

Definition at line 52 of file weight_constraint.h.

bool Clasp::WeightLitsRep::open ( ) const [inline]

Definition at line 51 of file weight_constraint.h.

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.

Definition at line 109 of file weight_constraint.cpp.

bool Clasp::WeightLitsRep::sat ( ) const [inline]

Definition at line 49 of file weight_constraint.h.

bool Clasp::WeightLitsRep::unsat ( ) const [inline]

Definition at line 50 of file weight_constraint.h.