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 #include "solvertypes.h" 24 #include "clause.h" 25 #include "propby.h" 26 #include "clauseallocator.h" 27 28 #ifndef __PROPBYFORGRAPH_H__ 29 #define __PROPBYFORGRAPH_H__ 30 31 namespace CMSat { 32 33 class PropByForGraph 34 { 35 private: 36 uint16_t type; 37 uint32_t isize; 38 Clause* clause; 39 Lit lits[3]; 40 41 public: PropByForGraph(PropBy orig,Lit otherLit,const ClauseAllocator & alloc)42 PropByForGraph(PropBy orig 43 , Lit otherLit 44 , const ClauseAllocator& alloc 45 ) : 46 type(10) 47 , isize(0) 48 , clause(NULL) 49 { 50 if (orig.getType() == binary_t) { 51 lits[0] = otherLit; 52 lits[1] = orig.lit2(); 53 type = 1; 54 isize = 2; 55 } 56 if (orig.isClause()) { 57 if (orig.isNULL()) { 58 type = 0; 59 isize = 0; 60 clause = NULL; 61 return; 62 } 63 clause = alloc.ptr(orig.get_offset()); 64 isize = clause->size(); 65 type = 0; 66 } 67 } 68 PropByForGraph()69 PropByForGraph() : 70 type(0) 71 , clause(NULL) 72 {} 73 PropByForGraph(const PropByForGraph & other)74 PropByForGraph(const PropByForGraph& other) : 75 type(other.type) 76 , isize(other.isize) 77 , clause(other.clause) 78 { 79 memcpy(lits, other.lits, sizeof(Lit)*3); 80 } 81 82 PropByForGraph& operator=(const PropByForGraph& other) 83 { 84 type = other.type, 85 isize = other.isize; 86 clause = other.clause; 87 //delete xorLits; 88 memcpy(lits, other.lits, sizeof(Lit)*3); 89 return *this; 90 } 91 size()92 uint32_t size() const 93 { 94 return isize; 95 } 96 isNULL()97 bool isNULL() const 98 { 99 return type == 0 && clause == NULL; 100 } 101 isClause()102 bool isClause() const 103 { 104 return type == 0; 105 } 106 isBin()107 bool isBin() const 108 { 109 return type == 1; 110 } 111 getClause()112 const Clause* getClause() const 113 { 114 return clause; 115 } 116 getClause()117 Clause* getClause() 118 { 119 return clause; 120 } 121 122 Lit operator[](const uint32_t i) const 123 { 124 switch (type) { 125 case 0: 126 assert(clause != NULL); 127 return (*clause)[i]; 128 129 default : 130 return lits[i]; 131 } 132 } 133 }; 134 135 inline std::ostream& operator<<( 136 std::ostream& os 137 , const PropByForGraph& propByFull 138 ) { 139 140 if (propByFull.isBin()) { 141 os << propByFull[0] << " " << propByFull[1]; 142 } else if (propByFull.isClause()) { 143 if (propByFull.isNULL()) os << "null clause"; 144 else os << *propByFull.getClause(); 145 } 146 return os; 147 } 148 149 } //end namespace 150 151 #endif //__PROPBYFORGRAPH_H__ 152