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/arithvar_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/arithvar_set.h')
-rw-r--r-- | src/theory/arith/arithvar_set.h | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index 0d59e3aea..4cd205172 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -72,9 +72,12 @@ public: return d_posVector.size(); } - void clear(){ + void purge() { + for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end();i!= endIter; ++i){ + d_posVector[*i] = ARITHVAR_SENTINEL; + } d_list.clear(); - d_posVector.clear(); + Assert(empty()); } void increaseSize(ArithVar max){ @@ -117,6 +120,16 @@ public: const_iterator begin() const{ return d_list.begin(); } const_iterator end() const{ return d_list.end(); } + /** + * Invalidates iterators. + * Adds x to the set if it is not already in the set. + */ + void softAdd(ArithVar x){ + if(!isMember(x)){ + add(x); + } + } + const VarList& getList() const{ return d_list; } @@ -125,8 +138,16 @@ public: void remove(ArithVar x){ Assert(isMember(x)); swapToBack(x); - d_posVector[x] = ARITHVAR_SENTINEL; + Assert(d_list.back() == x); + pop_back(); + } + + ArithVar pop_back() { + Assert(!empty()); + ArithVar atBack = d_list.back(); + d_posVector[atBack] = ARITHVAR_SENTINEL; d_list.pop_back(); + return atBack; } private: |