diff options
Diffstat (limited to 'src/prop/minisat/mtl')
-rw-r--r-- | src/prop/minisat/mtl/Alg.h | 18 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BasicHeap.h | 17 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BoxedVec.h | 43 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Heap.h | 26 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Map.h | 20 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Queue.h | 17 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Sort.h | 17 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Vec.h | 15 |
8 files changed, 128 insertions, 45 deletions
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index 240962dfc..e636f2b87 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -17,8 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Alg_h -#define Alg_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Alg_h +#define CVC4_MiniSat_Alg_h + +#include <cassert> + +namespace CVC4 { +namespace prop { +namespace minisat { //================================================================================================= // Useful functions on vectors @@ -54,4 +62,8 @@ static inline bool find(V& ts, const T& t) return j < ts.size(); } -#endif +}/* 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 556d98f84..cb6a7cbd8 100644 --- a/src/prop/minisat/mtl/BasicHeap.h +++ b/src/prop/minisat/mtl/BasicHeap.h @@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef BasicHeap_h -#define BasicHeap_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_BasicHeap_h +#define CVC4_MiniSat_BasicHeap_h #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -95,4 +101,9 @@ class BasicHeap { //================================================================================================= -#endif + +}/* 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 bddf41008..7cf5ba14f 100644 --- a/src/prop/minisat/mtl/BoxedVec.h +++ b/src/prop/minisat/mtl/BoxedVec.h @@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef BoxedVec_h -#define BoxedVec_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_BoxedVec_h +#define CVC4_MiniSat_BoxedVec_h #include <cstdlib> #include <cassert> #include <new> +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Automatically resizable arrays // @@ -50,7 +56,7 @@ class bvec { x->cap = size; return x; } - + }; Vec_t* ref; @@ -76,16 +82,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: @@ -107,11 +113,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 () { @@ -119,10 +125,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(); } @@ -143,5 +149,8 @@ public: }; +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ -#endif +#endif /* CVC4_MiniSat_BoxedVec_h */ diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index b07ccd152..20d379b1d 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -17,10 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Heap_h -#define Heap_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Heap_h +#define CVC4_MiniSat_Heap_h #include "Vec.h" +#include <cassert> + +namespace CVC4 { +namespace prop { +namespace minisat { //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -92,7 +99,7 @@ class Heap { indices[n] = heap.size(); heap.push(n); - percolateUp(indices[n]); + percolateUp(indices[n]); } @@ -104,19 +111,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); } @@ -164,6 +171,9 @@ class Heap { }; +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ //================================================================================================= -#endif +#endif /* CVC4_MiniSat_Heap_h */ diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index b6d76a31c..715b84da4 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Map_h -#define Map_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Map_h +#define CVC4_MiniSat_Map_h #include <stdint.h> #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Default hash/equals functions // @@ -80,7 +86,7 @@ class Map { cap = newsize; } - + public: Map () : table(NULL), cap(0), size(0) {} @@ -94,7 +100,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; } @@ -115,4 +121,8 @@ class Map { } }; -#endif +}/* 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 2cc110ce9..291a1f2e3 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Queue_h -#define Queue_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Queue_h +#define CVC4_MiniSat_Queue_h #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= @@ -79,4 +85,9 @@ public: //}; //================================================================================================= -#endif + +}/* 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 1f301f5c2..19e89803b 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Sort_h -#define Sort_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Sort_h +#define CVC4_MiniSat_Sort_h #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Some sorting algorithms for vec's @@ -90,4 +96,9 @@ template <class T> void sort(vec<T>& v) { //================================================================================================= -#endif + +}/* 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 e780aa167..364991aa9 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Vec_h -#define Vec_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Vec_h +#define CVC4_MiniSat_Vec_h #include <cstdlib> #include <cassert> #include <new> +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Automatically resizable arrays // @@ -129,5 +135,8 @@ void vec<T>::clear(bool dealloc) { sz = 0; if (dealloc) free(data), data = NULL, cap = 0; } } +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ -#endif +#endif /* CVC4_MiniSat_Vec_h */ |