#include <clasp/util/platform.h>
#include <clasp/pod_vector.h>
#include <algorithm>
#include <limits>
Go to the source code of this file.
Classes | |
class | Clasp::ClaspError |
struct | Clasp::SymbolTable::LessKey |
class | Clasp::Literal |
A literal is a variable or its negation. More... | |
struct | Clasp::SymbolTable::String |
struct | Clasp::SymbolTable::symbol_type |
class | Clasp::SymbolTable |
Symbol table that maps external ids to internal literals. More... | |
struct | Clasp::Var_t |
Possible types of a variable. More... | |
Namespaces | |
namespace | Clasp |
Typedefs | |
typedef PodVector< Literal >::type | Clasp::LitVec |
typedef PodVector< wsum_t >::type | Clasp::SumVec |
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. |
Contains the definition of the class Literal.
Definition in file literal.h.