1 | // Class automatically generated by Dev-C++ New Class wizard |
---|
2 | |
---|
3 | #ifndef ATOMSANDNODES_H |
---|
4 | #define ATOMSANDNODES_H |
---|
5 | |
---|
6 | #include <vector> |
---|
7 | |
---|
8 | #include <iostream> |
---|
9 | |
---|
10 | #include "../../Basics.h" |
---|
11 | #include <SomeTime.h> |
---|
12 | |
---|
13 | using namespace std; |
---|
14 | |
---|
15 | #define INVALID_DL -1 |
---|
16 | |
---|
17 | class CClauseVertex; |
---|
18 | typedef CClauseVertex *PCLV; |
---|
19 | |
---|
20 | class CVariableVertex; |
---|
21 | typedef CVariableVertex *PVARV; |
---|
22 | |
---|
23 | typedef unsigned int indexTypeVARS; |
---|
24 | typedef unsigned int indexTypeCLS; |
---|
25 | |
---|
26 | typedef indexTypeVARS VarIdT; |
---|
27 | typedef indexTypeCLS ClauseIdT; |
---|
28 | |
---|
29 | class LiteralIdT |
---|
30 | { |
---|
31 | indexTypeVARS val; |
---|
32 | public: |
---|
33 | |
---|
34 | LiteralIdT() |
---|
35 | { |
---|
36 | val = 0; |
---|
37 | } |
---|
38 | LiteralIdT(int iLitIdx) |
---|
39 | { |
---|
40 | val = (abs(iLitIdx)<<1) + (unsigned int)(iLitIdx > 0); |
---|
41 | } |
---|
42 | |
---|
43 | LiteralIdT(VarIdT iVarIdx, bool polarity) |
---|
44 | { |
---|
45 | val = (iVarIdx<<1) + (unsigned int)polarity; |
---|
46 | } |
---|
47 | |
---|
48 | VarIdT toVarIdx() const |
---|
49 | { |
---|
50 | return (val >> 1); |
---|
51 | } |
---|
52 | |
---|
53 | unsigned int toUInt() const |
---|
54 | { |
---|
55 | return val; |
---|
56 | } |
---|
57 | |
---|
58 | void makeFromUInt(unsigned int v) |
---|
59 | { |
---|
60 | val = v; |
---|
61 | } |
---|
62 | |
---|
63 | bool polarity() const |
---|
64 | { |
---|
65 | return (bool)(val & 0x01); |
---|
66 | } |
---|
67 | |
---|
68 | TriValue polarityTriVal() const |
---|
69 | { |
---|
70 | return (TriValue)(val & 0x01); |
---|
71 | } |
---|
72 | |
---|
73 | bool operator!=(const LiteralIdT &rL2) const |
---|
74 | { |
---|
75 | return val != rL2.val; |
---|
76 | } |
---|
77 | |
---|
78 | bool operator==(const LiteralIdT &rL2) const |
---|
79 | { |
---|
80 | return val == rL2.val; |
---|
81 | } |
---|
82 | |
---|
83 | const LiteralIdT oppositeLit() const |
---|
84 | { |
---|
85 | return LiteralIdT(toVarIdx(),!polarity()); |
---|
86 | } |
---|
87 | |
---|
88 | void print() const |
---|
89 | { |
---|
90 | toSTDOUT((polarity()?" ":"-")<< toVarIdx()<<" "); |
---|
91 | } |
---|
92 | }; |
---|
93 | |
---|
94 | |
---|
95 | static const ClauseIdT NOT_A_CLAUSE(0); |
---|
96 | static const LiteralIdT NOT_A_LIT(0,false); |
---|
97 | |
---|
98 | #define SENTINEL_CL NOT_A_CLAUSE |
---|
99 | #define SENTINEL_LIT NOT_A_LIT |
---|
100 | |
---|
101 | |
---|
102 | class CClauseVertex |
---|
103 | { |
---|
104 | /// the offset of the first literal of this clause in theLitVector of |
---|
105 | /// the main CInstanceGraph |
---|
106 | unsigned int litPoolOfs; |
---|
107 | |
---|
108 | LiteralIdT litA, litB; |
---|
109 | |
---|
110 | unsigned int numLits; |
---|
111 | int lastTouchTime; |
---|
112 | |
---|
113 | public: |
---|
114 | |
---|
115 | bool hasWatchLitA() { return litA != NOT_A_LIT;} |
---|
116 | bool hasWatchLitB() { return litB != NOT_A_LIT;} |
---|
117 | |
---|
118 | void setLitA(const LiteralIdT & lit) { litA = lit;} |
---|
119 | void setLitB(const LiteralIdT & lit) { litB = lit;} |
---|
120 | |
---|
121 | const LiteralIdT &idLitA() const {return litA;} |
---|
122 | const LiteralIdT &idLitB() const {return litB;} |
---|
123 | |
---|
124 | int getLastTouchTime() const |
---|
125 | { |
---|
126 | return lastTouchTime; |
---|
127 | } |
---|
128 | |
---|
129 | void setTouched() |
---|
130 | { |
---|
131 | lastTouchTime = CStepTime::getTime(); |
---|
132 | } |
---|
133 | |
---|
134 | void setLength(unsigned int nlen) |
---|
135 | { |
---|
136 | numLits = nlen; |
---|
137 | } |
---|
138 | unsigned int length() const |
---|
139 | { |
---|
140 | return numLits; |
---|
141 | } |
---|
142 | |
---|
143 | bool isDeleted() const |
---|
144 | { |
---|
145 | return numLits == 0; |
---|
146 | } |
---|
147 | |
---|
148 | void setDeleted() |
---|
149 | { |
---|
150 | numLits = 0; |
---|
151 | } |
---|
152 | |
---|
153 | |
---|
154 | void setLitOfs(unsigned int ofs) {litPoolOfs = ofs;} |
---|
155 | unsigned int getLitOfs() const {return litPoolOfs;} |
---|
156 | |
---|
157 | |
---|
158 | // class constructor |
---|
159 | CClauseVertex() |
---|
160 | { |
---|
161 | litA = litB = NOT_A_LIT; |
---|
162 | numLits = 0; |
---|
163 | litPoolOfs = 0; |
---|
164 | lastTouchTime =0; |
---|
165 | } |
---|
166 | |
---|
167 | void reset() |
---|
168 | { |
---|
169 | |
---|
170 | lastTouchTime = 0; |
---|
171 | } |
---|
172 | |
---|
173 | ~CClauseVertex(){} |
---|
174 | |
---|
175 | bool watches(const VarIdT &theVar) const |
---|
176 | { |
---|
177 | return (idLitA().toVarIdx() == theVar || idLitB().toVarIdx() == theVar); |
---|
178 | } |
---|
179 | |
---|
180 | }; |
---|
181 | |
---|
182 | |
---|
183 | |
---|
184 | |
---|
185 | |
---|
186 | template <typename _T> |
---|
187 | class extd_vector : public vector<_T> |
---|
188 | { |
---|
189 | |
---|
190 | |
---|
191 | public: |
---|
192 | void quickErase(int iOfs) |
---|
193 | { |
---|
194 | (*this)[iOfs] = vector<_T>::back(); |
---|
195 | vector<_T>::pop_back(); |
---|
196 | } |
---|
197 | |
---|
198 | //typename vector<_T>::iterator |
---|
199 | void quickErase(typename vector<_T>::iterator &it) |
---|
200 | { |
---|
201 | *it = vector<_T>::back(); |
---|
202 | vector<_T>::pop_back(); |
---|
203 | } |
---|
204 | |
---|
205 | }; |
---|
206 | |
---|
207 | |
---|
208 | |
---|
209 | class AntecedentT |
---|
210 | { |
---|
211 | unsigned int val; |
---|
212 | |
---|
213 | public: |
---|
214 | AntecedentT() { val = 1;} |
---|
215 | AntecedentT(const ClauseIdT idCl) |
---|
216 | { |
---|
217 | val = (idCl << 1) | 1; |
---|
218 | } |
---|
219 | AntecedentT(const LiteralIdT idLit) |
---|
220 | { |
---|
221 | val = (idLit.toUInt() << 1) ; |
---|
222 | } |
---|
223 | |
---|
224 | bool isAClause() {return val & 0x01;} |
---|
225 | |
---|
226 | ClauseIdT toCl() |
---|
227 | { |
---|
228 | return val>>1; |
---|
229 | } |
---|
230 | LiteralIdT toLit() |
---|
231 | { |
---|
232 | LiteralIdT idLit; |
---|
233 | idLit.makeFromUInt(val>>1); |
---|
234 | return idLit; |
---|
235 | } |
---|
236 | bool isAnt() { return (isAClause() && !(toCl() == NOT_A_CLAUSE)) |
---|
237 | || (!isAClause() && (toLit() != NOT_A_LIT));} |
---|
238 | |
---|
239 | }; |
---|
240 | |
---|
241 | class AntAndLit |
---|
242 | //structure saving a Lit and the antecedent implying it |
---|
243 | // antecedents may be clauses or literals |
---|
244 | { |
---|
245 | public: |
---|
246 | AntecedentT theAnt; |
---|
247 | LiteralIdT theLit; |
---|
248 | |
---|
249 | AntAndLit(const AntecedentT ant,const LiteralIdT pL) |
---|
250 | { |
---|
251 | theAnt = ant; |
---|
252 | theLit = pL; |
---|
253 | } |
---|
254 | |
---|
255 | AntAndLit(const LiteralIdT idAntLit,const LiteralIdT pL) |
---|
256 | { |
---|
257 | theAnt = AntecedentT(idAntLit); |
---|
258 | theLit = pL; |
---|
259 | } |
---|
260 | |
---|
261 | AntAndLit(const ClauseIdT idCl = NOT_A_CLAUSE,const LiteralIdT pL = 0) |
---|
262 | { |
---|
263 | theAnt = AntecedentT(idCl); |
---|
264 | theLit = pL; |
---|
265 | } |
---|
266 | |
---|
267 | AntecedentT &getAnt(){return theAnt;} |
---|
268 | LiteralIdT& getLit() {return theLit;} |
---|
269 | }; |
---|
270 | |
---|
271 | |
---|
272 | class CVariableVertex |
---|
273 | { |
---|
274 | /// INVARIANT : SENTINEL clclcl ... |
---|
275 | /// this is due to the watchCls being passed in reverse by BCP |
---|
276 | extd_vector<ClauseIdT> watchCls[2]; |
---|
277 | |
---|
278 | TriValue theVal; |
---|
279 | |
---|
280 | VarIdT itecIndex; |
---|
281 | |
---|
282 | AntecedentT myAntecedent; |
---|
283 | int DecLevelOfDeactivation; |
---|
284 | |
---|
285 | /// INVARIANT: array content: llll SENTINEL xxxxx SENTINEL |
---|
286 | /// x: conflict binary link |
---|
287 | vector<LiteralIdT> binClLinks[2]; // where the variable occurrs in pos/neg |
---|
288 | |
---|
289 | unsigned int inClsVecOfs[2]; // the offset in the theInClsVector |
---|
290 | unsigned int iVarNum; // the number the variable had in the input file |
---|
291 | |
---|
292 | |
---|
293 | public: |
---|
294 | |
---|
295 | void setInClsVecOfs(bool pol, unsigned int ofs) |
---|
296 | { |
---|
297 | inClsVecOfs[pol] = ofs; |
---|
298 | } |
---|
299 | |
---|
300 | void setInClsVecOfs(unsigned int ofs) |
---|
301 | { |
---|
302 | unsigned int diff = inClsVecOfs[true] - inClsVecOfs[false]; |
---|
303 | inClsVecOfs[false] = ofs; |
---|
304 | inClsVecOfs[true] = ofs + diff; |
---|
305 | } |
---|
306 | |
---|
307 | unsigned int getInClsVecOfs(bool pol) const |
---|
308 | { |
---|
309 | return inClsVecOfs[pol]; |
---|
310 | } |
---|
311 | |
---|
312 | |
---|
313 | int scoreDLIS[2]; |
---|
314 | int scoreVSIDS[2]; |
---|
315 | |
---|
316 | void eraseAllEdges() |
---|
317 | { |
---|
318 | inClsVecOfs[0] = 1; |
---|
319 | inClsVecOfs[1] = 1; |
---|
320 | |
---|
321 | watchCls[0].clear(); |
---|
322 | watchCls[0].push_back(SENTINEL_CL); |
---|
323 | watchCls[1].clear(); |
---|
324 | watchCls[1].push_back(SENTINEL_CL); |
---|
325 | |
---|
326 | binClLinks[0].clear(); |
---|
327 | binClLinks[0].push_back(SENTINEL_LIT); |
---|
328 | binClLinks[0].push_back(SENTINEL_LIT); |
---|
329 | binClLinks[1].clear(); |
---|
330 | binClLinks[1].push_back(SENTINEL_LIT); |
---|
331 | binClLinks[1].push_back(SENTINEL_LIT); |
---|
332 | } |
---|
333 | |
---|
334 | |
---|
335 | CVariableVertex(unsigned int numofVar = 0, VarIdT index = 0): itecIndex(index), iVarNum(numofVar) |
---|
336 | { |
---|
337 | DecLevelOfDeactivation = INVALID_DL; |
---|
338 | theVal=X; |
---|
339 | |
---|
340 | scoreDLIS[0] = scoreDLIS[1] = 0; |
---|
341 | scoreVSIDS[0] = scoreVSIDS[1] = 0; |
---|
342 | |
---|
343 | eraseAllEdges(); |
---|
344 | } |
---|
345 | |
---|
346 | bool isolated() {return (inClsVecOfs[0] <= 1) && (inClsVecOfs[1] <= 1) |
---|
347 | && (binClLinks[0].size()<=2) && (binClLinks[1].size()<=2);} |
---|
348 | |
---|
349 | LiteralIdT getLitIdT(bool polarity) {return LiteralIdT(getVarIdT(),polarity);} |
---|
350 | |
---|
351 | void newtecIndex(VarIdT iIdx) {itecIndex = iIdx;} |
---|
352 | |
---|
353 | int getDLCSScore() const {return scoreDLIS[0] + scoreDLIS[1];} |
---|
354 | |
---|
355 | int getVSIDSScore(){return scoreVSIDS[0] + scoreVSIDS[1];} |
---|
356 | |
---|
357 | inline const unsigned int getVarNum() const {return iVarNum;} |
---|
358 | |
---|
359 | inline const unsigned int getVarIdT() const {return itecIndex;} |
---|
360 | |
---|
361 | int getDLOD() const {return DecLevelOfDeactivation;} |
---|
362 | |
---|
363 | bool setVal(bool aVal,unsigned int atDL, AntecedentT ant = AntecedentT(NOT_A_CLAUSE)) |
---|
364 | { |
---|
365 | if(!isActive()) return false; |
---|
366 | DecLevelOfDeactivation = atDL; |
---|
367 | |
---|
368 | myAntecedent = ant; |
---|
369 | theVal = (TriValue) aVal; |
---|
370 | return true; |
---|
371 | } |
---|
372 | |
---|
373 | void unsetVal() |
---|
374 | { |
---|
375 | myAntecedent = AntecedentT(NOT_A_CLAUSE); |
---|
376 | DecLevelOfDeactivation = INVALID_DL; |
---|
377 | theVal = X; |
---|
378 | } |
---|
379 | |
---|
380 | bool isImpliedBy(const ClauseIdT idCl) |
---|
381 | { |
---|
382 | if(isActive() || !myAntecedent.isAClause()) return false; |
---|
383 | if(myAntecedent.toCl() == idCl) return true; |
---|
384 | return false; |
---|
385 | } |
---|
386 | void adjustAntecedent(AntecedentT ant) {myAntecedent=ant;} |
---|
387 | bool isActive() const {return theVal == X;} |
---|
388 | |
---|
389 | bool flipVal() |
---|
390 | { |
---|
391 | if(theVal == W) theVal =F; |
---|
392 | else if(theVal == F) theVal =W; |
---|
393 | |
---|
394 | return true; |
---|
395 | } |
---|
396 | |
---|
397 | AntecedentT getAntecedent() {return myAntecedent;} |
---|
398 | |
---|
399 | bool getboolVal() const {return theVal==W;} |
---|
400 | |
---|
401 | TriValue getVal() const {return theVal;} |
---|
402 | |
---|
403 | unsigned int countBinLinks() const {return binClLinks[0].size() + binClLinks[1].size() - 4;} |
---|
404 | unsigned int countBinLinks(bool pol) const {return binClLinks[pol].size() - 2;} |
---|
405 | |
---|
406 | |
---|
407 | extd_vector<ClauseIdT> &getWatchClauses(bool polarity) |
---|
408 | { |
---|
409 | return watchCls[polarity]; |
---|
410 | } |
---|
411 | |
---|
412 | const extd_vector<ClauseIdT> &getWatchClauses(bool polarity) const |
---|
413 | { |
---|
414 | return watchCls[polarity]; |
---|
415 | } |
---|
416 | |
---|
417 | void addWatchClause(ClauseIdT idCl,bool polarity) |
---|
418 | { |
---|
419 | watchCls[polarity].push_back(idCl); |
---|
420 | } |
---|
421 | |
---|
422 | void addBinLink(bool polarity, LiteralIdT &lit) |
---|
423 | { |
---|
424 | *(binClLinks[polarity].end()-2) = lit; |
---|
425 | binClLinks[polarity].push_back(SENTINEL_LIT); |
---|
426 | } |
---|
427 | |
---|
428 | void addBinLinkCCl(bool polarity, LiteralIdT &lit) |
---|
429 | { |
---|
430 | *(binClLinks[polarity].end()-1) = lit; |
---|
431 | binClLinks[polarity].push_back(SENTINEL_LIT); |
---|
432 | } |
---|
433 | |
---|
434 | bool eraseBinLinkTo(LiteralIdT idLit, bool Linkpolarity); |
---|
435 | bool hasBinLinkTo(LiteralIdT idLit,bool pol) const; |
---|
436 | |
---|
437 | const vector<LiteralIdT> & getBinLinks(bool polarity) const |
---|
438 | { |
---|
439 | return binClLinks[polarity]; |
---|
440 | } |
---|
441 | vector<LiteralIdT> & getBinLinks(bool polarity) |
---|
442 | { |
---|
443 | return binClLinks[polarity]; |
---|
444 | } |
---|
445 | |
---|
446 | bool eraseWatchClause(ClauseIdT idCl, bool polarity); |
---|
447 | |
---|
448 | bool substituteWatchCl(bool polarity, const ClauseIdT & oldId, const ClauseIdT &newId); |
---|
449 | |
---|
450 | bool substituteBinLink(bool polarity, const LiteralIdT& oldLit, const LiteralIdT& newLit); |
---|
451 | |
---|
452 | // class destructor |
---|
453 | ~CVariableVertex(); |
---|
454 | }; |
---|
455 | |
---|
456 | #endif |
---|
457 | |
---|