1 files changed, 20 insertions, 0 deletions
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 513300a32..f59c17dc0 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -23,6 +23,7 @@
 
 #include <utility>
 #include <vector>
+#include <algorithm>
 #include "expr/node.h"
 
 namespace CVC4 {
@@ -77,6 +78,25 @@ public:
   }
 
   /**
+   * Clear out the accumulated substitutions, resetting this
+   * SubstitutionMap to the way it was when first constructed.
+   */
+  void clear() {
+    d_substitutions.clear();
+    d_substitutionCache.clear();
+    d_cacheInvalidated = true;
+  }
+
+  /**
+   * Swap the contents of this SubstitutionMap with those of another.
+   */
+  void swap(SubstitutionMap& map) {
+    d_substitutions.swap(map.d_substitutions);
+    d_substitutionCache.swap(map.d_substitutionCache);
+    std::swap(d_cacheInvalidated, map.d_cacheInvalidated);
+  }
+
+  /**
    * Print to the output stream
    */
   void print(std::ostream& out) const;