1 //
2 // Copyright (c) 2006-2017 Benjamin Kaufmann
3 //
4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
5 //
6 // Permission is hereby granted, free of charge, to any person obtaining a copy
7 // of this software and associated documentation files (the "Software"), to
8 // deal in the Software without restriction, including without limitation the
9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
10 // sell copies of the Software, and to permit persons to whom the Software is
11 // furnished to do so, subject to the following conditions:
12 //
13 // The above copyright notice and this permission notice shall be included in
14 // all copies or substantial portions of the Software.
15 //
16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
22 // IN THE SOFTWARE.
23 //
24 #ifndef CLASP_LITERAL_H_INCLUDED
25 #define CLASP_LITERAL_H_INCLUDED
26
27 #ifdef _MSC_VER
28 #pragma once
29 #endif
30 #include <clasp/config.h>
31 #include <clasp/pod_vector.h>
32 #include <algorithm> // std::swap
33 #include <limits>
34 /*!
35 * \file
36 * \brief Types and functions related to literals and variables.
37 */
38 namespace Clasp {
39 /*!
40 * \addtogroup constraint
41 */
42 //@{
43
44 //! A variable is an integer in the range [0..varMax).
45 typedef uint32 Var;
46
47 //! varMax is not a valid variale, i.e. currently Clasp supports at most 2^30 variables.
48 const Var varMax = (Var(1) << 30);
49
50 //! The variable 0 has a special meaning in the solver.
51 const Var sentVar = 0;
52
53 //! Literal ids are in the range [0..litIdMax).
54 const uint32 litIdMax = (Var(1) << 31);
55
56 //! Possible types of a variable.
57 struct Var_t {
58 enum Type { Atom = 1, Body = 2, Hybrid = Atom | Body};
isBodyVar_t59 static bool isBody(Type t) {
60 return (static_cast<uint32>(t) & static_cast<uint32>(Body)) != 0;
61 }
isAtomVar_t62 static bool isAtom(Type t) {
63 return (static_cast<uint32>(t) & static_cast<uint32>(Atom)) != 0;
64 }
65 };
66 typedef Var_t::Type VarType;
67
68 //! A literal is a variable or its negation.
69 /*!
70 * \par Implementation:
71 * A literal's state is stored in a single 32-bit integer as follows:
72 * - 30-bits : variable id
73 * - 1-bit : sign, 1 if negative, 0 if positive
74 * - 1-bit : general purpose flag for marking a literal instance
75 */
76 class Literal {
77 public:
78 static const uint32 sign_bit = 2u;
79 static const uint32 flag_bit = 1u;
80
81 //! The default constructor creates the positive literal of the special sentinel var.
Literal()82 Literal() : rep_(0) { }
83
84 //! Creates a literal of the variable var with sign s.
85 /*!
86 * \param var The literal's variable.
87 * \param sign true if new literal should be negative.
88 * \pre var < varMax
89 */
Literal(Var var,bool sign)90 Literal(Var var, bool sign) : rep_( (var<<sign_bit) + (uint32(sign)<<flag_bit) ) {
91 assert( var < varMax );
92 }
93
94 //! Returns the variable of the literal.
var()95 Var var() const { return rep_ >> sign_bit; }
96
97 //! Returns the sign of the literal.
98 /*!
99 * \return true if the literal is negative. Otherwise false.
100 */
sign()101 bool sign() const { return (rep_ & sign_bit) != 0; }
102
103 //! Returns var and sign encoded in a unique id.
104 /*!
105 * \note The watch-flag is ignored and thus the id of a literal can be stored in 31-bits.
106 */
id()107 uint32 id() const { return rep_ >> flag_bit; }
108
109 //! Returns the stored representation of this literal.
rep()110 uint32& rep() { return rep_; }
rep()111 uint32 rep() const { return rep_; }
112
113 //! Creates a literal from an id.
fromId(uint32 id)114 static Literal fromId(uint32 id) {
115 assert(id < litIdMax);
116 return Literal(id<<flag_bit);
117 }
118 //! Creates a literal from an unsigned integer.
fromRep(uint32 rep)119 static Literal fromRep(uint32 rep) { return Literal(rep); }
120
swap(Literal & other)121 void swap(Literal& other) { std::swap(rep_, other.rep_); }
122
123 //! Sets the watched-flag of this literal.
flag()124 Literal& flag() { rep_ |= flag_bit; return *this; }
125
126 //! Clears the watched-flag of this literal.
unflag()127 Literal& unflag() { rep_ &= ~flag_bit; return *this; }
128
129 //! Returns true if the watched-flag of this literal is set.
flagged()130 bool flagged() const { return (rep_ & flag_bit) != 0; }
131
132 //! Returns the complimentary literal of this literal.
133 /*!
134 * The complementary Literal of a Literal is a Literal referring to the
135 * same variable but with inverted sign.
136 */
137 inline Literal operator~() const {
138 return Literal( (rep_ ^ sign_bit) & ~flag_bit );
139 }
140 private:
Literal(uint32 rep)141 Literal(uint32 rep) : rep_(rep) {}
142 uint32 rep_;
143 };
144 //! Equality-Comparison for literals.
145 inline bool operator==(const Literal& lhs, const Literal& rhs) {
146 return lhs.id() == rhs.id();
147 }
148 //! Defines a strict-weak-ordering for Literals.
149 inline bool operator<(const Literal& lhs, const Literal& rhs) {
150 return lhs.id() < rhs.id();
151 }
152 //! Returns !(lhs == rhs).
153 inline bool operator!=(const Literal& lhs, const Literal& rhs) {
154 return !(lhs == rhs);
155 }
156 inline Literal operator^(Literal lhs, bool sign) { return Literal::fromId( lhs.id() ^ uint32(sign) ); }
157 inline Literal operator^(bool sign, Literal rhs) { return rhs ^ sign; }
swap(Literal & l,Literal & r)158 inline void swap(Literal& l, Literal& r) { l.swap(r); }
159 //! Creates the negative literal of variable v.
negLit(Var v)160 inline Literal negLit(Var v) { return Literal(v, true); }
161 //! Creates the positive literal of variable v.
posLit(Var v)162 inline Literal posLit(Var v) { return Literal(v, false); }
163 //! Returns negLit(abs(p)) if p < 0 and posLit(p) otherwise.
toLit(int32 p)164 inline Literal toLit(int32 p) { return p < 0 ? negLit(static_cast<Var>(-p)) : posLit(static_cast<Var>(p)); }
165 //! Converts the given (non-sentinel) literal to a signed integer s.th. p == toLit(toInt(p)).
toInt(Literal p)166 inline int32 toInt(Literal p) { return p.sign() ? -static_cast<int32>(p.var()) : static_cast<int32>(p.var()); }
167 //! Always-true literal.
168 // TODO: replace with constant using constexpr ctor once we switch to C++11
lit_true()169 inline Literal lit_true() { return Literal(sentVar, false); }
170 //! Always-false literal.
171 // TODO: replace with constant using constexpr ctor once we switch to C++11
lit_false()172 inline Literal lit_false() { return Literal(sentVar, true); }
173 //! Returns true if p represents the special variable 0
isSentinel(Literal p)174 inline bool isSentinel(Literal p) { return p.var() == sentVar; }
175
176 // Low-level conversion between Literals and int literals.
177 // We cannot use toInt() here because it is not defined for the
178 // sentinel literals lit_true() and lit_false().
encodeLit(Literal x)179 inline int32 encodeLit(Literal x) { return !x.sign() ? static_cast<int32>(x.var()+1) : -static_cast<int32>(x.var()+1); }
decodeVar(int32 x)180 inline Var decodeVar(int32 x) { return static_cast<Var>(x >= 0 ? x : -x) - 1; }
decodeLit(int32 x)181 inline Literal decodeLit(int32 x) { return Literal(decodeVar(x), x < 0); }
182
hashId(unsigned key)183 inline unsigned hashId(unsigned key) {
184 key = ~key + (key << 15);
185 key ^= (key >> 11);
186 key += (key << 3);
187 key ^= (key >> 5);
188 key += (key << 10);
189 key ^= (key >> 16);
190 return key;
191 }
hashLit(Literal p)192 inline uint32 hashLit(Literal p) { return hashId(p.id()); }
193
194 //! A signed integer type used to represent weights.
195 typedef int32 weight_t;
196 //! A signed integer type used to represent sums of weights.
197 typedef int64 wsum_t;
198 #define CLASP_WEIGHT_T_MAX ( 2147483647)
199 #define CLASP_WEIGHT_T_MIN (-2147483647 - 1)
200 #define CLASP_WEIGHT_SUM_MAX INT64_MAX
201 #define CLASP_WEIGHT_SUM_MIN INT64_MIN
202
203 typedef PodVector<Var>::type VarVec; //!< A vector of variables.
204 typedef PodVector<Literal>::type LitVec; //!< A vector of literals.
205 typedef PodVector<weight_t>::type WeightVec; //!< A vector of weights.
206 typedef PodVector<wsum_t>::type SumVec; //!< A vector of sums of weights.
207 typedef std::pair<Literal, weight_t> WeightLiteral; //!< A literal associated with a weight.
208 typedef PodVector<WeightLiteral>::type WeightLitVec; //!< A vector of weight-literals.
209 ///////////////////////////////////////////////////////////////////////////////
210 // Truth values
211 ///////////////////////////////////////////////////////////////////////////////
212 typedef uint8 ValueRep; //!< Type of the three value-literals.
213 const ValueRep value_true = 1; //!< Value used for variables that are true.
214 const ValueRep value_false = 2; //!< Value used for variables that are false.
215 const ValueRep value_free = 0; //!< Value used for variables that are unassigned.
216 typedef PodVector<ValueRep>::type ValueVec;
217
218 //! Returns the value that makes the literal lit true.
219 /*!
220 * \param lit The literal for which the true-value should be determined.
221 * \return
222 * - value_true iff lit is a positive literal
223 * - value_false iff lit is a negative literal.
224 * .
225 */
trueValue(const Literal & lit)226 inline ValueRep trueValue(const Literal& lit) { return 1 + lit.sign(); }
227
228 //! Returns the value that makes the literal lit false.
229 /*!
230 * \param lit The literal for which the false-value should be determined.
231 * \return
232 * - value_false iff lit is a positive literal
233 * - value_true iff lit is a negative literal.
234 * .
235 */
falseValue(const Literal & lit)236 inline ValueRep falseValue(const Literal& lit) { return 1 + !lit.sign(); }
237
238 //! Returns the sign that matches the value.
239 /*!
240 * \return
241 * - false iff v == value_true
242 * - true otherwise
243 */
valSign(ValueRep v)244 inline bool valSign(ValueRep v) { return v != value_true; }
245 //@}
246 }
247 #endif
248