1 |
|
/****************************************** |
2 |
|
Copyright (c) 2016, Mate Soos |
3 |
|
|
4 |
|
Permission is hereby granted, free of charge, to any person obtaining a copy |
5 |
|
of this software and associated documentation files (the "Software"), to deal |
6 |
|
in the Software without restriction, including without limitation the rights |
7 |
|
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell |
8 |
|
copies of the Software, and to permit persons to whom the Software is |
9 |
|
furnished to do so, subject to the following conditions: |
10 |
|
|
11 |
|
The above copyright notice and this permission notice shall be included in |
12 |
|
all copies or substantial portions of the Software. |
13 |
|
|
14 |
|
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR |
15 |
|
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, |
16 |
|
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE |
17 |
|
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER |
18 |
|
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, |
19 |
|
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN |
20 |
|
THE SOFTWARE. |
21 |
|
***********************************************/ |
22 |
|
|
23 |
|
#ifndef __SOLVERTYPESMINI_H__ |
24 |
|
#define __SOLVERTYPESMINI_H__ |
25 |
|
|
26 |
|
#include <cstdint> |
27 |
|
#include <iostream> |
28 |
|
#include <cassert> |
29 |
|
#include <vector> |
30 |
|
|
31 |
|
namespace CMSat { |
32 |
|
|
33 |
|
constexpr uint32_t var_Undef(0xffffffffU >> 4); |
34 |
|
|
35 |
|
class TooManyVarsError {}; |
36 |
|
class TooLongClauseError {}; |
37 |
|
|
38 |
|
class Lit |
39 |
|
{ |
40 |
|
uint32_t x; |
41 |
30 |
constexpr explicit Lit(uint32_t i) : x(i) { } |
42 |
|
public: |
43 |
13 |
constexpr Lit() : x(var_Undef<<1) {} // (lit_Undef) |
44 |
9976 |
constexpr explicit Lit(uint32_t var, bool is_inverted) : |
45 |
9976 |
x(var + var + is_inverted) |
46 |
9976 |
{} |
47 |
|
|
48 |
|
constexpr const uint32_t& toInt() const { // Guarantees small, positive integers suitable for array indexing. |
49 |
|
return x; |
50 |
|
} |
51 |
30 |
constexpr Lit operator~() const { |
52 |
30 |
return Lit(x ^ 1); |
53 |
|
} |
54 |
|
constexpr Lit operator^(const bool b) const { |
55 |
|
return Lit(x ^ (uint32_t)b); |
56 |
|
} |
57 |
|
Lit& operator^=(const bool b) { |
58 |
|
x ^= (uint32_t)b; |
59 |
|
return *this; |
60 |
|
} |
61 |
30 |
constexpr bool sign() const { |
62 |
30 |
return x & 1; |
63 |
|
} |
64 |
30 |
constexpr uint32_t var() const { |
65 |
30 |
return x >> 1; |
66 |
|
} |
67 |
|
constexpr Lit unsign() const { |
68 |
|
return Lit(x & ~1U); |
69 |
|
} |
70 |
30 |
constexpr bool operator==(const Lit& p) const { |
71 |
30 |
return x == p.x; |
72 |
|
} |
73 |
|
constexpr bool operator!= (const Lit& p) const { |
74 |
|
return x != p.x; |
75 |
|
} |
76 |
|
/** |
77 |
|
@brief ONLY to be used for ordering such as: a, b, ~b, etc. |
78 |
|
*/ |
79 |
|
constexpr bool operator < (const Lit& p) const { |
80 |
|
return x < p.x; // '<' guarantees that p, ~p are adjacent in the ordering. |
81 |
|
} |
82 |
|
constexpr bool operator > (const Lit& p) const { |
83 |
|
return x > p.x; |
84 |
|
} |
85 |
|
constexpr bool operator >= (const Lit& p) const { |
86 |
|
return x >= p.x; |
87 |
|
} |
88 |
|
constexpr static Lit toLit(uint32_t data) |
89 |
|
{ |
90 |
|
return Lit(data); |
91 |
|
} |
92 |
|
}; |
93 |
|
|
94 |
|
static const Lit lit_Undef(var_Undef, false); // Useful special constants. |
95 |
|
static const Lit lit_Error(var_Undef, true ); // |
96 |
|
|
97 |
|
inline std::ostream& operator<<(std::ostream& os, const Lit lit) |
98 |
|
{ |
99 |
|
if (lit == lit_Undef) { |
100 |
|
os << "lit_Undef"; |
101 |
|
} else { |
102 |
|
os << (lit.sign() ? "-" : "") << (lit.var() + 1); |
103 |
|
} |
104 |
|
return os; |
105 |
|
} |
106 |
|
|
107 |
|
inline std::ostream& operator<<(std::ostream& co, const std::vector<Lit>& lits) |
108 |
|
{ |
109 |
|
for (uint32_t i = 0; i < lits.size(); i++) { |
110 |
|
co << lits[i]; |
111 |
|
|
112 |
|
if (i != lits.size()-1) |
113 |
|
co << " "; |
114 |
|
} |
115 |
|
|
116 |
|
return co; |
117 |
|
} |
118 |
|
|
119 |
|
class lbool { |
120 |
|
uint8_t value; |
121 |
|
|
122 |
|
public: |
123 |
|
constexpr explicit lbool(uint8_t v) : value(v) { } |
124 |
|
constexpr lbool() : value(0) { } |
125 |
|
constexpr explicit lbool(bool x) : value(!x) { } |
126 |
|
|
127 |
423 |
constexpr bool operator == (lbool b) const { |
128 |
423 |
return ((b.value & 2) & (value & 2)) | (!(b.value & 2) & (value == b.value)); |
129 |
|
} |
130 |
|
constexpr bool operator != (lbool b) const { |
131 |
|
return !(*this == b); |
132 |
|
} |
133 |
|
constexpr lbool operator ^ (bool b) const { |
134 |
|
return lbool((uint8_t)(value ^ (uint8_t)b)); |
135 |
|
} |
136 |
|
|
137 |
|
lbool operator && (lbool b) const { |
138 |
|
uint8_t sel = (value << 1) | (b.value << 3); |
139 |
|
uint8_t v = (0xF7F755F4 >> sel) & 3; |
140 |
|
return lbool(v); |
141 |
|
} |
142 |
|
|
143 |
|
lbool operator || (lbool b) const { |
144 |
|
uint8_t sel = (value << 1) | (b.value << 3); |
145 |
|
uint8_t v = (0xFCFCF400 >> sel) & 3; |
146 |
|
return lbool(v); |
147 |
|
} |
148 |
|
|
149 |
|
constexpr uint8_t getValue() const { return value; } |
150 |
|
|
151 |
|
friend lbool toLbool(uint32_t v); |
152 |
|
constexpr friend uint32_t toInt (lbool l); |
153 |
|
}; |
154 |
|
|
155 |
|
constexpr lbool l_True = lbool((uint8_t)0); |
156 |
|
constexpr lbool l_False = lbool((uint8_t)1); |
157 |
|
constexpr lbool l_Undef = lbool((uint8_t)2); |
158 |
|
|
159 |
|
inline lbool toLbool(uint32_t v) |
160 |
|
{ |
161 |
|
lbool l; |
162 |
|
l.value = v; |
163 |
|
return l; |
164 |
|
} |
165 |
|
|
166 |
|
|
167 |
|
constexpr inline uint32_t toInt (lbool l) |
168 |
|
{ |
169 |
|
return l.value; |
170 |
|
} |
171 |
|
|
172 |
|
inline lbool boolToLBool(const bool b) |
173 |
|
{ |
174 |
|
if (b) { |
175 |
|
return l_True; |
176 |
|
} else { |
177 |
|
return l_False; |
178 |
|
} |
179 |
|
} |
180 |
|
|
181 |
|
inline std::ostream& operator<<(std::ostream& cout, const lbool val) |
182 |
|
{ |
183 |
|
if (val == l_True) cout << "l_True"; |
184 |
|
if (val == l_False) cout << "l_False"; |
185 |
|
if (val == l_Undef) cout << "l_Undef"; |
186 |
|
return cout; |
187 |
|
} |
188 |
|
|
189 |
|
enum class rst_dat_type {norm, var, cl}; |
190 |
|
|
191 |
|
} |
192 |
|
|
193 |
|
#endif //__SOLVERTYPESMINI_H__ |