This commit merges the arith-prop-opt branch into the main trunk. This was done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out.

1 files changed, 35 insertions, 0 deletions

diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
new file mode 100644
index 000000000..fa606188a
--- /dev/null
+++ b/src/theory/arith/ordered_set.h
@@ -0,0 +1,35 @@
+#include <set>
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "util/Assert.h"
+
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+struct RightHandRationalLT
+{
+  bool operator()(TNode s1, TNode s2) const
+  {
+    TNode rh1 = s1[1];
+    TNode rh2 = s2[1];
+    const Rational& c1 = rh1.getConst<Rational>();
+    const Rational& c2 = rh2.getConst<Rational>();
+    int cmpRes = c1.cmp(c2);
+    return cmpRes < 0;
+  }
+};
+
+typedef std::set<Node, RightHandRationalLT> OrderedSet;
+
+struct SetCleanupStrategy{
+  static void cleanup(OrderedSet* l){
+    Debug("arithgc") << "cleaning up  " << l << "\n";
+    delete l;
+  }
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */