No commit message

Lib/ArrayMap.hpp

@@ -134,6 +134,19 @@ class ArrayMap
     return (*this)[index]._obj;
   }
 
+  /**
+   * Return the object assigned to key @b index or @b def if there isn't any.
+   */
+  inline
+  T get(size_t index, T def)
+  {
+    CALL("ArrayMap::get");
+    if((*this)[index]._timestamp!=_timestamp) {
+      return def;
+    }
+    return (*this)[index]._obj;
+  }
+
   /**
    * Return @b true if key @b index has an object assigned
    *

Lib/Stack.hpp

@@ -18,12 +18,17 @@
 #include "Allocator.hpp"
 #include "Backtrackable.hpp"
 
+namespace std
+{
+template<typename T>
+void swap(Lib::Stack<T>& s1, Lib::Stack<T>& s2);
+}
+
 namespace Lib {
 
 template<typename C>
 struct Relocator<Stack<C> >;
 
-
 /**
  * Class of flexible-size generic stacks.
  * @since 11/03/2006 Bellevue
@@ -34,6 +39,9 @@ template<class C>
 class Stack
 {
 public:
+  template<typename U>
+  friend void std::swap(Stack<U>&,Stack<U>&);
+
   class Iterator;
 
   DECL_ELEMENT_TYPE(C);
@@ -691,4 +699,20 @@ struct Relocator<Stack<C> >
 
 } // namespace Lib
 
+namespace std
+{
+
+template<typename T>
+void swap(Lib::Stack<T>& s1, Lib::Stack<T>& s2)
+{
+  CALL("std::swap(Stack&,Stack&)");
+
+  swap(s1._capacity, s2._capacity);
+  swap(s1._cursor, s2._cursor);
+  swap(s1._end, s2._end);
+  swap(s1._stack, s2._stack);
+}
+
+}
+
 #endif

Makefile

@@ -205,6 +205,7 @@ VINF_OBJ=Inferences/BackwardDemodulation.o\
 
 VSAT_OBJ=SAT/ClauseDisposer.o\
          SAT/DIMACS.o\
+         SAT/ISSatSweeping.o\
          SAT/MinimizingSolver.o\
          SAT/Preprocess.o\
          SAT/RestartStrategy.o\