diff options
Diffstat (limited to 'src/theory/arith/ordered_set.h')
-rw-r--r-- | src/theory/arith/ordered_set.h | 79 |
1 files changed, 74 insertions, 5 deletions
diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index 68c5e18c9..43ccd7815 100644 --- 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 */ |