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