1 /****************************************** 2 Copyright (c) 2019, Armin Biere 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 VMTF_H 24 25 #include <vector> 26 #include <cstdint> 27 using std::vector; 28 29 namespace CMSat { 30 31 struct Link { 32 // variable indices 33 uint32_t prev = std::numeric_limits<uint32_t>::max(); 34 uint32_t next = std::numeric_limits<uint32_t>::max(); 35 }; 36 37 typedef vector<Link> Links; 38 39 struct Queue { 40 41 // We use integers instead of variable pointers. This is more compact and 42 // also avoids issues due to moving the variable table during 'resize'. 43 44 uint32_t first, last; // anchors (head/tail) for doubly linked list 45 uint32_t unassigned; // all variables after this one are assigned 46 uint64_t vmtf_bumped; // see vmtf_update_queue_unassigned 47 QueueQueue48 Queue () : 49 first (std::numeric_limits<uint32_t>::max()), 50 last (std::numeric_limits<uint32_t>::max()), 51 unassigned (std::numeric_limits<uint32_t>::max()), 52 vmtf_bumped (std::numeric_limits<uint64_t>::max()) 53 {} 54 55 // We explicitly provide the mapping of integer indices to vmtf_links to the 56 // following two (inlined) functions. This avoids including 57 // 'internal.hpp' and breaks a cyclic dependency, so we can keep their 58 // code here in this header file. Otherwise they are just ordinary doubly 59 // linked list 'dequeue' and 'enqueue' operations. 60 dequeueQueue61 inline void dequeue (Links & vmtf_links, uint32_t idx) { 62 Link & l = vmtf_links[idx]; 63 64 if (l.prev != std::numeric_limits<uint32_t>::max()) { 65 vmtf_links[l.prev].next = l.next; 66 } else { 67 first = l.next; 68 } 69 70 if (l.next != std::numeric_limits<uint32_t>::max()) { 71 vmtf_links[l.next].prev = l.prev; 72 } else { 73 last = l.prev; 74 } 75 } 76 enqueueQueue77 inline void enqueue (Links & vmtf_links, uint32_t idx) { 78 Link & l = vmtf_links[idx]; 79 l.prev = last; 80 if (l.prev != std::numeric_limits<uint32_t>::max()) { 81 vmtf_links[last].next = idx; 82 } else { 83 first = idx; 84 } 85 last = idx; 86 l.next = std::numeric_limits<uint32_t>::max(); 87 } 88 }; 89 90 } //namespace 91 92 #endif //VMTF_H 93