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 PROPBY_H 24 #define PROPBY_H 25 26 #include "constants.h" 27 #include "solvertypes.h" 28 #include "clause.h" 29 30 //#define DEBUG_PROPAGATEFROM 31 32 #include "cloffset.h" 33 34 namespace CMSat { 35 36 enum PropByType {null_clause_t = 0, clause_t = 1, binary_t = 2, tertiary_t = 3}; 37 38 class PropBy 39 { 40 private: 41 uint32_t data1; 42 uint32_t data2; 43 44 //0: clause, NULL 45 //1: clause, non-null 46 //2: binary 47 //3: tertiary 48 char type; 49 50 char red_step; 51 52 public: PropBy()53 PropBy() : 54 red_step(0) 55 , data1(0) 56 , type(null_clause_t) 57 , data2(0) 58 {} 59 60 //Normal clause prop PropBy(const ClOffset offset)61 explicit PropBy(const ClOffset offset) : 62 red_step(0) 63 , data1(offset) 64 , type(clause_t) 65 , data2(0) 66 { 67 //No roll-over 68 /*#ifdef DEBUG_PROPAGATEFROM 69 assert(offset == get_offset()); 70 #endif*/ 71 } 72 73 //Binary prop PropBy(const Lit lit,const bool redStep)74 PropBy(const Lit lit, const bool redStep) : 75 red_step(redStep) 76 , data1(lit.toInt()) 77 , type(binary_t) 78 , data2(0) 79 { 80 } 81 82 //For hyper-bin, etc. PropBy(const Lit lit,bool redStep,bool hyperBin,bool hyperBinNotAdded)83 PropBy( 84 const Lit lit 85 , bool redStep //Step that lead here from ancestor is redundant 86 , bool hyperBin //It's a hyper-binary clause 87 , bool hyperBinNotAdded //It's a hyper-binary clause, but was never added because all the rest was zero-level 88 ) : 89 red_step(redStep) 90 , data1(lit.toInt()) 91 , type(binary_t) 92 , data2(0) 93 { 94 //HACK: if we are doing seamless hyper-bin and transitive reduction 95 //then if we are at toplevel, .getAncestor() 96 //must work, and return lit_Undef, but at the same time, .isNULL() 97 //must also work, for conflict generation. So this is a hack to 98 //achieve that. What an awful hack. 99 if (lit == ~lit_Undef) 100 type = null_clause_t; 101 102 data2 = ((uint32_t)hyperBin) << 1 103 | ((uint32_t)hyperBinNotAdded) << 2; 104 } 105 106 //Tertiary prop PropBy(const Lit lit1,const Lit lit2,const bool redStep)107 PropBy(const Lit lit1, const Lit lit2, const bool redStep) : 108 red_step(redStep) 109 , data1(lit1.toInt()) 110 , type(tertiary_t) 111 , data2(lit2.toInt()) 112 { 113 } 114 isRedStep()115 bool isRedStep() const 116 { 117 return red_step; 118 } 119 getHyperbin()120 bool getHyperbin() const 121 { 122 return data2 & 2U; 123 } 124 setHyperbin(bool toSet)125 void setHyperbin(bool toSet) 126 { 127 data2 &= ~2U; 128 data2 |= (uint32_t)toSet << 1; 129 } 130 getHyperbinNotAdded()131 bool getHyperbinNotAdded() const 132 { 133 return data2 & 4U; 134 } 135 setHyperbinNotAdded(bool toSet)136 void setHyperbinNotAdded(bool toSet) 137 { 138 data2 &= ~4U; 139 data2 |= (uint32_t)toSet << 2; 140 } 141 getAncestor()142 Lit getAncestor() const 143 { 144 #ifdef DEBUG_PROPAGATEFROM 145 assert(type == null_clause_t || type == binary_t); 146 #endif 147 return ~Lit::toLit(data1); 148 } 149 isClause()150 bool isClause() const 151 { 152 return type == clause_t; 153 } 154 getType()155 PropByType getType() const 156 { 157 return (PropByType)type; 158 } 159 lit2()160 Lit lit2() const 161 { 162 #ifdef DEBUG_PROPAGATEFROM 163 assert(type == tertiary_t || type == binary_t); 164 #endif 165 return Lit::toLit(data1); 166 } 167 lit3()168 Lit lit3() const 169 { 170 #ifdef DEBUG_PROPAGATEFROM 171 assert(type == tertiary_t); 172 #endif 173 return Lit::toLit(data2); 174 } 175 get_offset()176 ClOffset get_offset() const 177 { 178 #ifdef DEBUG_PROPAGATEFROM 179 assert(isClause()); 180 #endif 181 return data1; 182 } 183 isNULL()184 bool isNULL() const 185 { 186 return type == null_clause_t; 187 } 188 189 bool operator==(const PropBy other) const 190 { 191 return (type == other.type 192 && red_step == other.red_step 193 && data1 == other.data1 194 && data2 == other.data2 195 ); 196 } 197 198 bool operator!=(const PropBy other) const 199 { 200 return !(*this == other); 201 } 202 }; 203 204 inline std::ostream& operator<<(std::ostream& os, const PropBy& pb) 205 { 206 switch (pb.getType()) { 207 case binary_t : 208 os << " binary, other lit= " << pb.lit2(); 209 break; 210 211 case tertiary_t : 212 os << " tri, other 2 lits= " << pb.lit2() << " , "<< pb.lit3(); 213 break; 214 215 case clause_t : 216 os << " clause, num= " << pb.get_offset(); 217 break; 218 219 case null_clause_t : 220 os << " NULL"; 221 break; 222 223 default: 224 assert(false); 225 break; 226 } 227 return os; 228 } 229 230 } //end namespace 231 232 #endif //PROPBY_H 233