Adding the changes to the original copy

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 */