diff options
Diffstat (limited to 'src/prop/minisat/mtl')
-rw-r--r-- | src/prop/minisat/mtl/Alg.h | 8 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BasicHeap.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BoxedVec.h | 34 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Heap.h | 17 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Map.h | 10 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Queue.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Sort.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Vec.h | 6 |
8 files changed, 56 insertions, 37 deletions
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index a4ca4403b..0fe6d84c7 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -20,8 +20,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef CVC4_MiniSat_Alg_h #define CVC4_MiniSat_Alg_h +#include <cassert> + namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Useful functions on vectors @@ -57,7 +60,8 @@ static inline bool find(V& ts, const T& t) return j < ts.size(); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Alg_h */ diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h index b22a35ada..39d825411 100644 --- a/src/prop/minisat/mtl/BasicHeap.h +++ b/src/prop/minisat/mtl/BasicHeap.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -99,7 +100,8 @@ class BasicHeap { //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_BasicHeap_h */ diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h index 7c5b10e4c..05b801004 100644 --- a/src/prop/minisat/mtl/BoxedVec.h +++ b/src/prop/minisat/mtl/BoxedVec.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <new> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Automatically resizable arrays @@ -53,7 +54,7 @@ class bvec { x->cap = size; return x; } - + }; Vec_t* ref; @@ -79,16 +80,16 @@ class bvec { altvec (altvec<T>& other) { assert(0); } public: - void clear (bool dealloc = false) { + void clear (bool dealloc = false) { if (ref != NULL){ - for (int i = 0; i < ref->sz; i++) + for (int i = 0; i < ref->sz; i++) (*ref).data[i].~T(); - if (dealloc) { - free(ref); ref = NULL; - }else + if (dealloc) { + free(ref); ref = NULL; + }else ref->sz = 0; - } + } } // Constructors: @@ -110,11 +111,11 @@ public: int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); + ref = Vec_t::alloc(ref, cap); } - //new (&ref->data[size]) T(elem); - ref->data[size] = elem; - ref->sz = size+1; + //new (&ref->data[size]) T(elem); + ref->data[size] = elem; + ref->sz = size+1; } void push () { @@ -122,10 +123,10 @@ public: int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); + ref = Vec_t::alloc(ref, cap); } - new (&ref->data[size]) T(); - ref->sz = size+1; + new (&ref->data[size]) T(); + ref->sz = size+1; } void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } @@ -146,7 +147,8 @@ public: }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_BoxedVec_h */ diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index 84234705c..0c2019b65 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -21,9 +21,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define CVC4_MiniSat_Heap_h #include "Vec.h" +#include <cassert> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -95,7 +97,7 @@ class Heap { indices[n] = heap.size(); heap.push(n); - percolateUp(indices[n]); + percolateUp(indices[n]); } @@ -107,19 +109,19 @@ class Heap { indices[x] = -1; heap.pop(); if (heap.size() > 1) percolateDown(0); - return x; + return x; } - void clear(bool dealloc = false) - { + void clear(bool dealloc = false) + { for (int i = 0; i < heap.size(); i++) indices[heap[i]] = -1; #ifdef NDEBUG for (int i = 0; i < indices.size(); i++) assert(indices[i] == -1); #endif - heap.clear(dealloc); + heap.clear(dealloc); } @@ -167,7 +169,8 @@ class Heap { }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ //================================================================================================= diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index f69fca6d5..9168dde0e 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Default hash/equals functions @@ -83,7 +84,7 @@ class Map { cap = newsize; } - + public: Map () : table(NULL), cap(0), size(0) {} @@ -97,7 +98,7 @@ class Map { for (int i = 0; i < ps.size(); i++) if (equals(ps[i].key, k)){ d = ps[i].data; - return true; } + return true; } return false; } @@ -118,7 +119,8 @@ class Map { } }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Map_h */ diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index e4e7e2159..e02ac7222 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= @@ -83,7 +84,8 @@ public: //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Queue_h */ diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index df5261a06..2b9d5bb15 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Some sorting algorithms for vec's @@ -94,7 +95,8 @@ template <class T> void sort(vec<T>& v) { //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Sort_h */ diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index 1a07cc334..fae1d0c5d 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <new> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Automatically resizable arrays @@ -132,7 +133,8 @@ void vec<T>::clear(bool dealloc) { sz = 0; if (dealloc) free(data), data = NULL, cap = 0; } } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Vec_h */ |