Classes | Typedefs | Functions | Variables
Boolean Constraints

Classes

struct  Clasp::Activity
 Type storing a constraint's activity. More...
class  Clasp::ClauseCreator
 A helper-class for creating/adding clauses. More...
class  Clasp::Constraint
 Base class for (boolean) constraints to be used in a Solver. More...
struct  Clasp::Constraint_t
 Constraint types distinguished by a Solver. More...
class  Clasp::DefaultUnfoundedCheck
 Clasp's default unfounded set checker. More...
class  Clasp::LearntConstraint
 Base class for learnt constraints. More...
class  Clasp::Literal
 A literal is a variable or its negation. More...
class  Clasp::LoopFormula
 Constraint for Loop-Formulas. More...
class  Clasp::MessageHandler
class  Clasp::MinimizeConstraint
 Base class for implementing (mulit-level) minimize statements. More...
class  Clasp::PostPropagator
 Base class for post propagators. More...
struct  Clasp::Var_t
 Possible types of a variable. More...
class  Clasp::WeightConstraint
 Class implementing smodels-like cardinality- and weight constraints. More...

Typedefs

typedef Constraint_t::Type Clasp::ConstraintType
typedef PodVector< Literal >::type Clasp::LitVec
typedef PodVector< wsum_t >::type Clasp::SumVec
typedef Constraint_t::Set Clasp::TypeSet
typedef uint8 Clasp::ValueRep
typedef PodVector< ValueRep >::type Clasp::ValueVec
typedef uint32 Clasp::Var
 A variable is currently nothing more but an integer in the range [0..varMax).
typedef Var_t::Type Clasp::VarType
typedef PodVector< Var >::type Clasp::VarVec
typedef int32 Clasp::weight_t
 A signed integer type used to represent weights.
typedef std::pair< Literal,
weight_t > 
Clasp::WeightLiteral
typedef PodVector
< WeightLiteral >::type 
Clasp::WeightLitVec
typedef PodVector< weight_t >::type Clasp::WeightVec
typedef int64 Clasp::wsum_t
 A signed integer type used to represent sums of weights.

Functions

ValueRep Clasp::falseValue (const Literal &lit)
 Returns the value that makes the literal lit false.
uint32 Clasp::index (Var v)
 Returns the index of variable v.
bool Clasp::isSentinel (Literal p)
 Returns true if p represents the special variable 0.
Literal Clasp::negLit (Var v)
 Creates the negative literal of variable v.
bool Clasp::operator!= (const Literal &lhs, const Literal &rhs)
 Returns !(lhs == rhs).
bool Clasp::operator< (const Literal &lhs, const Literal &rhs)
 Defines a strict-weak-ordering for Literals.
Literal Clasp::operator^ (Literal lhs, bool sign)
Literal Clasp::operator^ (bool sign, Literal rhs)
Literal Clasp::posLit (Var v)
 Creates the positive literal of variable v.
void Clasp::swap (Literal &l, Literal &r)
ValueRep Clasp::trueValue (const Literal &lit)
 Returns the value that makes the literal lit true.
bool Clasp::valSign (ValueRep v)
 Returns the sign that matches the value.

Variables

const uint32 Clasp::idMax = UINT32_MAX
 Ids are integers in the range [0..idMax).
const Var Clasp::sentVar = 0
 The variable 0 has a special meaning in the solver.
const ValueRep Clasp::value_false = 2
const ValueRep Clasp::value_free = 0
const ValueRep Clasp::value_true = 1
const Var Clasp::varMax = (Var(1) << 30)
 varMax is not a valid variale, i.e. currently Clasp supports at most 2^30 variables.

Typedef Documentation

typedef Constraint_t::Type Clasp::ConstraintType

Definition at line 64 of file constraint.h.

typedef PodVector<Literal>::type Clasp::LitVec

A vector of literals.

Definition at line 193 of file literal.h.

typedef PodVector<wsum_t>::type Clasp::SumVec

A vector of sums of weights.

Definition at line 195 of file literal.h.

typedef Constraint_t::Set Clasp::TypeSet

Definition at line 65 of file constraint.h.

typedef uint8 Clasp::ValueRep

Type of the three value-literals.

Definition at line 203 of file literal.h.

typedef PodVector<ValueRep>::type Clasp::ValueVec

Definition at line 207 of file literal.h.

typedef uint32 Clasp::Var

A variable is currently nothing more but an integer in the range [0..varMax).

Definition at line 42 of file literal.h.

typedef Var_t::Type Clasp::VarType

Definition at line 63 of file literal.h.

typedef PodVector<Var>::type Clasp::VarVec

A vector of variables.

Definition at line 192 of file literal.h.

typedef int32 Clasp::weight_t

A signed integer type used to represent weights.

Definition at line 66 of file literal.h.

typedef std::pair<Literal, weight_t> Clasp::WeightLiteral

A weight-literal.

Definition at line 197 of file literal.h.

typedef PodVector<WeightLiteral>::type Clasp::WeightLitVec

A vector of weight-literals.

Definition at line 198 of file literal.h.

typedef PodVector<weight_t>::type Clasp::WeightVec

A vector of weights.

Definition at line 194 of file literal.h.

typedef int64 Clasp::wsum_t

A signed integer type used to represent sums of weights.

Definition at line 68 of file literal.h.


Function Documentation

ValueRep Clasp::falseValue ( const Literal &  lit) [inline]

Returns the value that makes the literal lit false.

Parameters:
litThe literal for which the false-value should be determined.
Returns:
  • value_false iff lit is a positive literal
  • value_true iff lit is a negative literal.

Definition at line 227 of file literal.h.

uint32 Clasp::index ( Var  v) [inline]

Returns the index of variable v.

Note:
same as posLit(v).index()

Definition at line 173 of file literal.h.

bool Clasp::isSentinel ( Literal  p) [inline]

Returns true if p represents the special variable 0.

Definition at line 176 of file literal.h.

Literal Clasp::negLit ( Var  v) [inline]

Creates the negative literal of variable v.

Definition at line 166 of file literal.h.

bool Clasp::operator!= ( const Literal &  lhs,
const Literal &  rhs 
) [inline]

Returns !(lhs == rhs).

Definition at line 184 of file literal.h.

bool Clasp::operator< ( const Literal &  lhs,
const Literal &  rhs 
) [inline]

Defines a strict-weak-ordering for Literals.

Definition at line 179 of file literal.h.

Literal Clasp::operator^ ( Literal  lhs,
bool  sign 
) [inline]

Definition at line 159 of file literal.h.

Literal Clasp::operator^ ( bool  sign,
Literal  rhs 
) [inline]

Definition at line 160 of file literal.h.

Literal Clasp::posLit ( Var  v) [inline]

Creates the positive literal of variable v.

Definition at line 168 of file literal.h.

void Clasp::swap ( Literal &  l,
Literal &  r 
) [inline]

Definition at line 188 of file literal.h.

ValueRep Clasp::trueValue ( const Literal &  lit) [inline]

Returns the value that makes the literal lit true.

Parameters:
litThe literal for which the true-value should be determined.
Returns:
  • value_true iff lit is a positive literal
  • value_false iff lit is a negative literal.

Definition at line 217 of file literal.h.

bool Clasp::valSign ( ValueRep  v) [inline]

Returns the sign that matches the value.

Returns:
  • false iff v == value_true
  • true otherwise

Definition at line 235 of file literal.h.


Variable Documentation

const uint32 Clasp::idMax = UINT32_MAX

Ids are integers in the range [0..idMax).

Definition at line 51 of file literal.h.

const Var Clasp::sentVar = 0

The variable 0 has a special meaning in the solver.

Definition at line 48 of file literal.h.

const ValueRep Clasp::value_false = 2

Value used for variables that are false.

Definition at line 205 of file literal.h.

const ValueRep Clasp::value_free = 0

Value used for variables that are unassigned.

Definition at line 206 of file literal.h.

const ValueRep Clasp::value_true = 1

Value used for variables that are true.

Definition at line 204 of file literal.h.

const Var Clasp::varMax = (Var(1) << 30)

varMax is not a valid variale, i.e. currently Clasp supports at most 2^30 variables.

Definition at line 45 of file literal.h.



clasp
Author(s): Benjamin Kaufmann
autogenerated on Thu Aug 27 2015 12:41:40