diff options
author | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
commit | abe849b486ea3707fd51a612c7982554f3d6581f (patch) | |
tree | 8f3967f644f9098079c778dd60cf9feb36e1ab2b /src/theory/arith/ordered_set.h | |
parent | b90081962840584bb9eeda368ea232a7d42a292b (diff) |
This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
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 */ |