summaryrefslogtreecommitdiff
path: root/src/theory/arith/arithvar_set.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/arithvar_set.h')
-rw-r--r--src/theory/arith/arithvar_set.h372
1 files changed, 0 insertions, 372 deletions
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
deleted file mode 100644
index b9ae48b16..000000000
--- a/src/theory/arith/arithvar_set.h
+++ /dev/null
@@ -1,372 +0,0 @@
-/********************* */
-/*! \file arithvar_set.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
-#define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
-
-#include <vector>
-#include "theory/arith/arithvar.h"
-#include "context/context.h"
-#include "context/cdlist.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-/**
- * This is an abstraction of a set of ArithVars.
- * This class is designed to provide constant time insertion, deletion, and element_of
- * and fast iteration.
- *
- * ArithVarSets come in 2 varieties: ArithVarSet, and PermissiveBackArithVarSet.
- * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars
- * that are greater than allocated(). Asking isMember() of such an ArithVar
- * is an assertion failure. The cost of doing this is that it takes O(M)
- * where M is the total number of ArithVars in memory.
- *
- * PermissiveBackArithVarSet means that all ArithVars are implicitly not in the set,
- * and any ArithVar past the end of d_posVector is not in the set.
- * A permissiveBack allows for less memory to be consumed on average.
- *
- */
-template <bool permissiveBack>
-class ArithVarSetImpl {
-public:
- typedef std::vector<ArithVar> VarList;
-private:
- //List of the ArithVars in the set.
- VarList d_list;
-
- //Each ArithVar in the set is mapped to its position in d_list.
- //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
- std::vector<unsigned> d_posVector;
-
-public:
- typedef VarList::const_iterator const_iterator;
-
- ArithVarSetImpl() : d_list(), d_posVector() {}
-
- size_t size() const {
- return d_list.size();
- }
- bool empty() const {
- return d_list.empty();
- }
-
- size_t allocated() const {
- return d_posVector.size();
- }
-
- 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();
- Assert(empty());
- }
-
- void increaseSize(ArithVar max){
- Assert(max >= allocated());
- d_posVector.resize(max+1, ARITHVAR_SENTINEL);
- }
-
- void increaseSize(){
- increaseSize(allocated());
- }
-
- bool isMember(ArithVar x) const{
- if(permissiveBack && x >= allocated()){
- return false;
- }else{
- Assert(x < allocated());
- return d_posVector[x] != ARITHVAR_SENTINEL;
- }
- }
-
- /** Invalidates iterators */
- void init(ArithVar x, bool val) {
- Assert(x >= allocated());
- increaseSize(x);
- if(val){
- add(x);
- }
- }
-
- /** Invalidates iterators */
- void add(ArithVar x){
- Assert(!isMember(x));
- if(permissiveBack && x >= allocated()){
- increaseSize(x);
- }
- d_posVector[x] = size();
- d_list.push_back(x);
- }
-
- 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;
- }
-
- /** Invalidates iterators */
- void remove(ArithVar x){
- Assert(isMember(x));
- swapToBack(x);
- 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:
-
- /** This should be true of all x < allocated() after every operation. */
- bool wellFormed(ArithVar x){
- if(d_posVector[x] == ARITHVAR_SENTINEL){
- return true;
- }else{
- return d_list[d_posVector[x]] == x;
- }
- }
-
- /** Swaps a member x to the back of d_list. */
- void swapToBack(ArithVar x){
- Assert(isMember(x));
-
- unsigned currentPos = d_posVector[x];
- ArithVar atBack = d_list.back();
-
- d_list[currentPos] = atBack;
- d_posVector[atBack] = currentPos;
-
- d_list[size() - 1] = x;
- d_posVector[x] = size() - 1;
- }
-};
-
-typedef ArithVarSetImpl<false> ArithVarSet;
-typedef ArithVarSetImpl<true> PermissiveBackArithVarSet;
-
-
-/**
- * ArithVarMultiset
- */
-class ArithVarMultiset {
-public:
- typedef std::vector<ArithVar> VarList;
-private:
- //List of the ArithVars in the multi set.
- VarList d_list;
-
- //Each ArithVar in the set is mapped to its position in d_list.
- //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
- std::vector<unsigned> d_posVector;
-
- //Count of the number of elements in the array
- std::vector<unsigned> d_counts;
-
-public:
- typedef VarList::const_iterator const_iterator;
-
- ArithVarMultiset() : d_list(), d_posVector() {}
-
- size_t size() const {
- return d_list.size();
- }
-
- bool empty() const {
- return d_list.empty();
- }
-
- size_t allocated() const {
- Assert(d_posVector.size() == d_counts.size());
- return d_posVector.size();
- }
-
- void purge() {
- for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end(); i!= endIter; ++i){
- d_posVector[*i] = ARITHVAR_SENTINEL;
- d_counts[*i] = 0;
- }
- d_list.clear();
- Assert(empty());
- }
-
- void increaseSize(ArithVar max){
- Assert(max >= allocated());
- d_posVector.resize(max+1, ARITHVAR_SENTINEL);
- d_counts.resize(max+1, 0);
- }
-
- void increaseSize(){
- increaseSize(allocated());
- }
-
- bool isMember(ArithVar x) const{
- if( x >= allocated()){
- return false;
- }else{
- Assert(x < allocated());
- return d_posVector[x] != ARITHVAR_SENTINEL;
- }
- }
-
- /**
- * Invalidates iterators.
- */
- void addMultiset(ArithVar x){
- if( x >= allocated()){
- increaseSize(x);
- }
- if(d_counts[x] == 0){
- d_posVector[x] = size();
- d_list.push_back(x);
- }
- d_counts[x]++;
- }
-
- unsigned count(ArithVar x){
- if( x >= allocated()){
- return 0;
- }else{
- return d_counts[x];
- }
- }
-
- const_iterator begin() const{ return d_list.begin(); }
- const_iterator end() const{ return d_list.end(); }
-
- const VarList& getList() const{
- return d_list;
- }
-
- /** Invalidates iterators */
- void remove(ArithVar x){
- Assert(isMember(x));
- swapToBack(x);
- Assert(d_list.back() == x);
- pop_back();
- }
-
- ArithVar pop_back() {
- Assert(!empty());
- ArithVar atBack = d_list.back();
- d_posVector[atBack] = ARITHVAR_SENTINEL;
- d_counts[atBack] = 0;
- d_list.pop_back();
- return atBack;
- }
-
- private:
-
- /** This should be true of all x < allocated() after every operation. */
- bool wellFormed(ArithVar x){
- if(d_posVector[x] == ARITHVAR_SENTINEL){
- return true;
- }else{
- return d_list[d_posVector[x]] == x;
- }
- }
-
- /** Swaps a member x to the back of d_list. */
- void swapToBack(ArithVar x){
- Assert(isMember(x));
-
- unsigned currentPos = d_posVector[x];
- ArithVar atBack = d_list.back();
-
- d_list[currentPos] = atBack;
- d_posVector[atBack] = currentPos;
-
- d_list[size() - 1] = x;
- d_posVector[x] = size() - 1;
- }
-};
-
-class CDArithVarSet {
-private:
-
- class RemoveIntCleanup {
- private:
- std::vector<bool>& d_set;
- public:
- RemoveIntCleanup(std::vector<bool>& set)
- : d_set(set)
- {}
-
- void operator()(ArithVar* p){
- ArithVar x = *p;
- Assert(d_set[x]);
- d_set[x] = false;
- }
- };
-
- std::vector<bool> d_set;
- context::CDList<ArithVar, RemoveIntCleanup> d_list;
-
-public:
- CDArithVarSet(context::Context* c)
- : d_set(), d_list(c, true, RemoveIntCleanup(d_set))
- { }
-
- /** This cannot be const as garbage collection is done lazily. */
- bool contains(ArithVar x) const{
- if(x < d_set.size()){
- return d_set[x];
- }else{
- return false;
- }
- }
-
- void insert(ArithVar x){
- Assert(!contains(x));
- if(x >= d_set.size()){
- d_set.resize(x+1, false);
- }
- d_list.push_back(x);
- d_set[x] = true;
- }
-};
-
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback