1/******************************************
2Copyright (c) 2016, Mate Soos
3
4Permission is hereby granted, free of charge, to any person obtaining a copy
5of this software and associated documentation files (the "Software"), to deal
6in the Software without restriction, including without limitation the rights
7to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8copies of the Software, and to permit persons to whom the Software is
9furnished to do so, subject to the following conditions:
10
11The above copyright notice and this permission notice shall be included in
12all copies or substantial portions of the Software.
13
14THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20THE 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
31namespace CMSat {
32
33constexpr uint32_t var_Undef(0xffffffffU >> 4);
34
35class TooManyVarsError {};
36class TooLongClauseError {};
37
38class Lit
39{
40    uint32_t x;
41    constexpr explicit Lit(uint32_t i) : x(i) { }
42public:
43    constexpr Lit() : x(var_Undef<<1) {}   // (lit_Undef)
44    constexpr explicit Lit(uint32_t var, bool is_inverted) :
45        x(var + var + is_inverted)
46    {}
47
48    constexpr const uint32_t& toInt() const { // Guarantees small, positive integers suitable for array indexing.
49        return x;
50    }
51    constexpr Lit  operator~() const {
52        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    constexpr bool sign() const {
62        return x & 1;
63    }
64    constexpr uint32_t  var() const {
65        return x >> 1;
66    }
67    constexpr Lit  unsign() const {
68        return Lit(x & ~1U);
69    }
70    constexpr bool operator==(const Lit& p) const {
71        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
94static const Lit lit_Undef(var_Undef, false);  // Useful special constants.
95static const Lit lit_Error(var_Undef, true );  //
96
97inline 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
107inline 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
119class lbool {
120    uint8_t value;
121
122public:
123    constexpr explicit lbool(uint8_t v) : value(v) { }
124    constexpr lbool()       : value(0) { }
125    constexpr explicit lbool(bool x) : value(!x) { }
126
127    constexpr bool  operator == (lbool b) const {
128        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
155constexpr lbool l_True = lbool((uint8_t)0);
156constexpr lbool l_False = lbool((uint8_t)1);
157constexpr lbool l_Undef = lbool((uint8_t)2);
158
159inline lbool toLbool(uint32_t v)
160{
161    lbool l;
162    l.value = v;
163    return l;
164}
165
166
167constexpr inline uint32_t toInt  (lbool l)
168{
169    return l.value;
170}
171
172inline lbool boolToLBool(const bool b)
173{
174    if (b) {
175        return l_True;
176    } else {
177        return l_False;
178    }
179}
180
181inline 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
189enum class rst_dat_type {norm, var, cl};
190
191}
192
193#endif //__SOLVERTYPESMINI_H__
194