This commit merges the branch arithmetic/propagation-again into trunk.

[cvc5.git] / src / theory / arith / ordered_set.h

diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index 68c5e18c9140929e0e928379ceb22ca57e8d8a2f..43ccd7815dca8395b6d9c79eb6f103419deae152 100644 (file)
--- a/src/theory/arith/ordered_set.h
+++ b/src/theory/arith/ordered_set.h
@@ -1,3 +1,4 @@
+#include <map>
 #include <set>
 #include "expr/kind.h"
 #include "expr/node.h"
@@ -9,16 +10,84 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+inline const Rational& rightHandRational(TNode ineq){
+  Assert(ineq.getKind() == kind::LEQ
+         || ineq.getKind() == kind::GEQ
+         || ineq.getKind() == kind::EQUAL);
+  TNode righthand = ineq[1];
+  Assert(righthand.getKind() == kind::CONST_RATIONAL);
+  return righthand.getConst<Rational>();
+}
 
-typedef std::set<TNode, RightHandRationalLT> OrderedSet;
+class BoundValueEntry {
+private:
+  const Rational& value;
+  TNode d_leq, d_geq;
 
-struct SetCleanupStrategy{
-  static void cleanup(OrderedSet* l){
-    Debug("arithgc") << "cleaning up  " << l << "\n";
-    delete l;
+  BoundValueEntry(const Rational& v, TNode l, TNode g):
+    value(v),
+    d_leq(l),
+    d_geq(g)
+  {}
+
+public:
+  Node getLeq() const{
+    Assert(hasLeq());
+    return d_leq;
+  }
+  Node getGeq() const{
+    Assert(hasGeq());
+    return d_geq;
+  }
+
+  static BoundValueEntry mkFromLeq(TNode leq){
+    Assert(leq.getKind() == kind::LEQ);
+    return BoundValueEntry(rightHandRational(leq), leq, TNode::null());
+  }
+
+  static BoundValueEntry mkFromGeq(TNode geq){
+    Assert(geq.getKind() == kind::GEQ);
+    return BoundValueEntry(rightHandRational(geq), TNode::null(), geq);
+  }
+
+  void addLeq(TNode leq){
+    Assert(leq.getKind() == kind::LEQ);
+    Assert(rightHandRational(leq) == getValue());
+    Assert(!hasLeq());
+    d_leq = leq;
+  }
+
+  void addGeq(TNode geq){
+    Assert(geq.getKind() == kind::GEQ);
+    Assert(rightHandRational(geq) == getValue());
+    Assert(!hasGeq());
+    d_geq = geq;
+  }
+
+  bool hasGeq() const { return d_geq != TNode::null(); }
+  bool hasLeq() const { return d_leq != TNode::null(); }
+
+
+  const Rational& getValue() const{
+    return value;
+  }
+
+  bool operator<(const BoundValueEntry& other){
+    return value < other.value;
   }
 };
 
+typedef std::map<Rational, BoundValueEntry> BoundValueSet;
+
+typedef std::set<TNode, RightHandRationalLT> EqualValueSet;
+
+// struct SetCleanupStrategy{
+//   static void cleanup(OrderedSet* l){
+//     Debug("arithgc") << "cleaning up  " << l << "\n";
+//     delete l;
+//   }
+// };
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */