2 files changed, 43 insertions, 2 deletions
diff --git a/src/prop/sat_solver_types.cpp b/src/prop/sat_solver_types.cpp
new file mode 100644
index 000000000..078c5d54d
--- /dev/null
+++ b/src/prop/sat_solver_types.cpp
@@ -0,0 +1,28 @@
+/*********************                                                        */
+/*! \file sat_solver_types.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementations of SAT solver type operations which require large
+ ** std headers.
+ **
+ **/
+
+#include "prop/sat_solver_types.h"
+
+#include <algorithm>
+
+namespace CVC4 {
+namespace prop {
+bool SatClauseLessThan::operator()(const SatClause& l, const SatClause& r) const
+{
+  return std::lexicographical_compare(l.begin(), l.end(), r.begin(), r.end());
+}
+}  // namespace prop
+}  // namespace CVC4
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index f1fd6233e..51d0c4cd5 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -122,6 +122,16 @@ public:
   }
 
   /**
+   * Compare two literals
+   */
+  bool operator<(const SatLiteral& other) const
+  {
+    return getSatVariable() == other.getSatVariable()
+               ? isNegated() < other.isNegated()
+               : getSatVariable() < other.getSatVariable();
+  }
+
+  /**
    * Returns a string representation of the literal.
    */
   std::string toString() const {
@@ -183,6 +193,11 @@ struct SatClauseSetHashFunction
   }
 };
 
+struct SatClauseLessThan
+{
+  bool operator()(const SatClause& l, const SatClause& r) const;
+};
+
 /**
  * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
  * so that the SAT solver can (or should) remove them when the lifespan is over.
@@ -221,5 +236,3 @@ enum SatSolverLifespan
 
 }
 }
-
-